|
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
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)>>
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.
|
|