Verification of a Microcomputer Program Specification Embedded in a Reactive System
スポンサーリンク
概要
- 論文の詳細を見る
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 reallife 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.
- 社団法人電子情報通信学会の論文
- 2000-05-25
著者
-
Ishihara Yasunori
The Author Is With Department Of Informatics And Mathematical Science Graduate School Of Engineering
-
NINOMIYA Kiichiro
The authors are with Electronic Engineering Laboratory, Daikin Industries, Ltd.
-
SEKI Hiroyuki
The authors are with Graduate School of Information Science, Nara Institute of Science and Technolog
-
TAKAHARA Daisuke
The authors are with Graduate School of Information Science, Nara Institute of Science and Technolog
-
YAMADA Yutaka
The authors are with Electronic Engineering Laboratory, Daikin Industries, Ltd.
-
OMOTO Shigesada
The authors are with Electronic Engineering Laboratory, Daikin Industries, Ltd.
-
Omoto Shigesada
The Authors Are With Electronic Engineering Laboratory Daikin Industries Ltd.
-
Takahara Daisuke
The Authors Are With Graduate School Of Information Science Nara Institute Of Science And Technology
-
Ninomiya Kiichiro
The Authors Are With Electronic Engineering Laboratory Daikin Industries Ltd.
-
Seki Hiroyuki
The Authors Are With Graduate School Of Information Science Nara Institute Of Science And Technology
-
Yamada Yutaka
The Authors Are With Electronic Engineering Laboratory Daikin Industries Ltd.
関連論文
- Verification of a Microcomputer Program Specification Embedded in a Reactive System
- Efficient Recognition Algorithms for Parallel Multiple Context-Free Languages and for Multiple Context-Free Languages