Verification of a Microcomputer Program Specification Embedded in a Reactive System

Yasunori ISHIHARA  Kiichiro NINOMIYA  Hiroyuki SEKI  Daisuke TAKAHARA  Yutaka YAMADA  Shigesada OMOTO  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E83-D   No.5   pp.1082-1091
Publication Date: 2000/05/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software Engineering
Keyword: 
compositional verification,  model checking,  reactive system,  reachability graph,  

Full Text: PDF(806.3KB)>>
Buy this Article



Summary: 
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.