Applying model checking to destructive testing and analysis of software system

被引：2

作者：

Kumamoto, Hiroki ^{[1
]}

Mizuno, Takahisa ^{[1
]}

Narita, Kensuke ^{[1
]}

Nishizaki, Shin-ya ^{[1
]}

机构：

[1] Department of Computer Science, Tokyo Institute of Technology, Tokyo

来源：

Journal of Software | 2013年 / 8卷 / 05期

基金：

日本学术振兴会;

关键词：

Fault tolerance; Model checking; Promela; Software verification; SPIN model checker;

D O I：

10.4304/jsw.8.5.1254-1261

中图分类号：

学科分类号：

摘要：

Recently, model checking is widely applied to software and hardware verification. It can locate hard-to- find bugs in systems by exhaustively searching executing paths. In this paper, we propose a new software design method that enables us to evaluate the fault tolerance of software behavior at the specification level: we can check software behavior, not only when the hardware and network are in good order, but also when they are out of order; we can then improve fault tolerance of the target software using the model checker. We can test software under environments in which we destroy hardware and/or networks intentionally in computer simulation. The method is explained by taking an example of a network-connected AV appliance. We model the AV appliance by the modeling language Promela and analyze it by the SPIN model checker. © 2013 ACADEMY PUBLISHER.

引用

页码：1254 / 1261

页数：7

共 15 条

[1] Holzmann G.J., The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, (2003)
[2] Pettersson P., Larsen K.G., UPPAAL2k, Bulletin of the European Association For Theoretical Computer Science, 70, pp. 40-44, (2000)
[3] Huth M., Ryan M., Logic In Computer Science: Modelling and Reasoning About System, (2004)
[4] Denning P.J., Fault tolerant operating systems, ACM Computing Surveys, 8, 4, pp. 359-389, (1976)
[5] Randell B., Lee P., Treleaven P.C., Reliability issues in computing system design, ACM Computing Surveys, 10, 2, pp. 123-165, (1978)
[6] Booch G., Rumbaugh J., Jacobson I., Unified Modeling Language User Guide, (2005)
[7] Tomioka D., Nishizaki S., Ikeda R., A cost estimation calculus for analyzing the resistance to denial-of-service attack, Software Security-Theories and Systems, 3233, pp. 25-44, (2004)
[8] Ikeda R., Narita K., Nishizaki S., Cooperation of model checking and network simulation for cost analysis of distributed system, International Journal of Computers and Applications, 33, 4, pp. 323-329, (2011)
[9] Nishizaki S., Tamano H., Design of Open Equation Archive Server Resistant Against Denial-of-Service Attacks, Accepted and To Appear In the Proceedings of International Conference On Advances In Information Technology and Mobile Communication-AIM2012
[10] Sasajima T., Nishizaki S., Blog-based Distributed Computation - Implementation of Software Verification System, Accepted and To Appear In the Proceedings of the 3rd International Conference On Information Computing and Applications ICICA2012, (2012)

← 1 2 →