Improving software model checking on program backbone within distributed system

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

研究成果: Conference contribution

抄録

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.

本文言語English
ホスト出版物のタイトル2014 IEEE International Conference on Information and Automation, ICIA 2014
出版社Institute of Electrical and Electronics Engineers Inc.
ページ35-40
ページ数6
ISBN(電子版)9781479941001
DOI
出版ステータスPublished - 2014 10 21
イベント2014 IEEE International Conference on Information and Automation, ICIA 2014 - Hailar, Hulunbuir, China
継続期間: 2014 7 282014 7 30

出版物シリーズ

名前2014 IEEE International Conference on Information and Automation, ICIA 2014

Conference

Conference2014 IEEE International Conference on Information and Automation, ICIA 2014
国/地域China
CityHailar, Hulunbuir
Period14/7/2814/7/30

ASJC Scopus subject areas

  • モデリングとシミュレーション

フィンガープリント

「Improving software model checking on program backbone within distributed system」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル