N-PAT: A Nested Model-Checker (System Description)

被引：3

作者：

Bride, Hadrien ^{[1
]}

Cai, Cheng-Hao ^{[2
]}

Dong, Jin Song ^{[1
,3
]}

Gore, Rajeev ^{[4
]}

Hou, Zhe ^{[1
]}

Mahony, Brendan ^{[5
]}

McCarthy, Jim ^{[5
]}

机构：

[1] Griffith Univ, Inst Integrated & Intelligent Syst, Brisbane, Qld, Australia

[2] Univ Auckland, Sch Comp Sci, Auckland, New Zealand

[3] Natl Univ Singapore, Sch Comp, Singapore, Singapore

[4] Australian Natl Univ, Res Sch Comp Sci, Canberra, ACT, Australia

[5] Def Sci & Technol, Canberra, ACT, Australia

来源：

AUTOMATED REASONING, PT II | 2020年 / 12167卷

关键词：

D O I：

10.1007/978-3-030-51054-1_22

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.

引用

页码：369 / 377

页数：9

共 10 条

[1]

Clarke E. M., 2018, HDB MODEL CHECKING, V10, DOI DOI 10.1007/978-3-319-10575-8

[2]

Clarke E. M., 2012, TOOLS PRACTICAL SOFT, P1, DOI [DOI 10.1007/978-3-642-35746-6_1, 10.1007/978-3-642-35746-61]

[3] COMMUNICATING SEQUENTIAL PROCESSES [J].

HOARE, CAR .

COMMUNICATIONS OF THE ACM, 1978, 21 (08) :666-677

[4]

Lopez-Fernandez J. J., 2014, ACM IEEE INT C AUT S, P831, DOI [10.1145/2642937.2648617, DOI 10.1145/2642937.2648617]

[5] A Novel Method to Verify Multilevel Computational Models of Biological Systems Using Multiscale Spatio-Temporal Meta Model Checking [J].

Parvu, Ovidiu ;

Gilbert, David .

PLOS ONE, 2016, 11 (05)

[6] M3C: Modal Meta Model Checking [J].

Steffen, Bernhard ;

Murtovi, Alnis .

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2018, 2018, 11119 :223-241

[7] Modeling and Verifying Hierarchical Real-Time Systems Using Stateful Timed CSP [J].

Sun, Jun ;

Liu, Yang ;

Dong, Jin Song ;

Liu, Yan ;

Shi, Ling ;

Andre, Etienne .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2013, 22 (01)

[8]

Sun J, 2010, LECT NOTES COMPUT SC, V6447, P388, DOI 10.1007/978-3-642-16901-4_26

[9]

Sun J, 2009, LECT NOTES COMPUT SC, V5885, P581, DOI 10.1007/978-3-642-10373-5_30

[10]

Sun J, 2008, COMM COM INF SC, V17, P307

← 1 →