Model Checking Analysis of Observational Transition System with SMV

被引：0

作者：

He, Tao ^{[1
]}

Li, Huazhong ^{[1
]}

Qin, Guorong ^{[1
]}

机构：

[1] Shenzhen Inst Informat Technol, Software Engn Dept, Shenzhen, Peoples R China

来源：

INFORMATION COMPUTING AND APPLICATIONS, PT II | 2011年 / 244卷

关键词：

Model Checking; Model-based verification; SMV; CafeOBJ; Model Checking Tool; VERIFICATION;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Model checking is an important way in developing high confidence systems. A model checking method basing on theorem proving is proposed in this paper, which describes the infinite system state by CafeOBJ and transfers a CafeOBJ specification to a finite SMV specification, and its tool has been implemented. It mainly observes transition system and shows that a counter example of a corresponding SMV specification is also a counter example of a CafeOBJ specification. It can find errors lurked in systems at earlier stages of their development processes to avoid spending much money and time to correct errors later.

引用

页码：537 / 544

页数：8

共 10 条

[1] Carew D., 2005, 2005 International Symposium on Empirical Software Engineering (IEEE Cat. No. 05EX1213)
[2] Cimatti A., 2002, Computer Aided Verification. 14th International Conference, CAV 2002. Proceedings (Lecture Notes in Computer Science Vol.2404), P359
[3] Diaconescu R, 2008, MONOGR THEOR COMPUT, P153, DOI 10.1007/978-3-540-74107-7_4
[4] A semantic part generated Java']Java statement from a CafeOBJ specification
Doungsa-ard, C.
Suwannasart, T.
[J]. 2006 IEEE INTERNATIONAL CONFERENCE ON ELECTRO/INFORMATION TECHNOLOGY, 2006, : 388 - 393
[5] Futatsugi K, 2010, LECT NOTES COMPUT SC, V6447, P1, DOI 10.1007/978-3-642-16901-4_1
[6] Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
Kong, Weiqiang
Ogata, Kazuhiro
Futatsugi, Kokichi
[J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2010, E93D (05) : 974 - 984
[7] Mapping template semantics to SMV
Lu, Y
Atlee, JM
Day, NA
Niu, JW
[J]. 19TH INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2004, : 320 - 325
[8] Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method
Ogata, Kazuhiro
Futatsugi, Kokichi
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 201 : 127 - 154
[9] Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method
Ouranos, Iakovos
Stefaneas, Petros
Ogata, Kazuhiro
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I, 2010, 6415 : 75 - +
[10] Action Language verifier: an infinite-state model checker for reactive software specifications
Yavuz-Kahveci, Tuba
Bultan, Tevfik
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2009, 35 (03) : 325 - 367

← 1 →