Improving software model checking on program backbone within distributed system

Jiawei Yong, Keiichi Koyanagi, Takeshi Tsuchiya, Tetsuyasu Yamada, Hiroaki Sawano

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Model checking technique currently has been applied to a wide range of problem domains. Among them, verifying the reliability of software systems becomes much more significant. However, as to software with complex structure and large scale, the verification process suffers from the state space explosion, thus leading to the resource exhaustion and low efficiency. In this paper, we propose a method of improving software model checking in both foreground and background of ANSI-C source program to verify the properties. In the foreground stage, we directly dispose of program itself by pruning the program with respect to the assertion property and compressing the circular paths to extract the program backbone. Subsequently, the program backbone is used to generate a simple CTL automaton model which will be applied afterwards. In the background stage, we redesign the CTL state automaton's data structure and improve the model checking algorithm to adapt the MapReduce framework in distributed system. The set of states which are satisfied with CTL property is output and checked for satisfiability based on the CTL automaton model. The example in each part illustrates the validity of the whole method, and the experiments show this method improves the efficiency of program verification substantially.

Original languageEnglish
Title of host publication2014 IEEE International Conference on Information and Automation, ICIA 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages35-40
Number of pages6
ISBN (Print)9781479941001
DOIs
Publication statusPublished - 2014 Oct 21
Event2014 IEEE International Conference on Information and Automation, ICIA 2014 - Hailar, Hulunbuir
Duration: 2014 Jul 282014 Jul 30

Other

Other2014 IEEE International Conference on Information and Automation, ICIA 2014
CityHailar, Hulunbuir
Period14/7/2814/7/30

    Fingerprint

Keywords

  • Distributed system
  • Program backbone
  • Software Model Checking

ASJC Scopus subject areas

  • Modelling and Simulation

Cite this

Yong, J., Koyanagi, K., Tsuchiya, T., Yamada, T., & Sawano, H. (2014). Improving software model checking on program backbone within distributed system. In 2014 IEEE International Conference on Information and Automation, ICIA 2014 (pp. 35-40). [6932622] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICInfA.2014.6932622