For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Verification of a Microcomputer Program Specification Embedded in a Reactive System
Yasunori ISHIHARA Kiichiro NINOMIYA Hiroyuki SEKI Daisuke TAKAHARA Yutaka YAMADA Shigesada OMOTO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2000/05/25
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software Engineering
compositional verification, model checking, reactive system, reachability graph,
Full Text: PDF(806.3KB)>>
This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem, we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough to cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.