空調機用マイコンソフトの形式的仕様記述と検証法について  [in Japanese] A formal specification and verification method for microcomputer software embedded in an air-conditioner  [in Japanese]

筆者らの研究グループでは, 空調機用マイコンプログラムを対象とした仕様検証システムを開発している. 実用規模の仕様を検証するには, 作成される到達可能性グラフのサイズが大きくなるという状態爆発の問題を解決しなくてはならない. そこで本稿では, 入力された仕様から検証項目に関連する部分だけを抽出し, それに対する到達可能性グラフを作成して検証を行う手法を提案する. 具体的には, 検証項目(論理式)ψが全称閉論理式のある部分クラスに属するとき, 条件「ψが部分仕様に対して成り立つならば, ψは入力仕様に対しても成り立つ」を満たす部分仕様の抽出法を与えている. さらに, 実際の空調機用マイコンソフトの機能要求を, 検証項目としてその部分クラスの論理式で記述できるかどうかについても述べる.

The authors are developing a system for verifying a specification of microcomputer software embedded in an air-conditioner. For such real-life specifications, a verification based on reachability analysis often fails because of the state-explosion. In this paper, we define verified formulas as a subclass of universally quantified, closed formulas. Then we propose a method of extracting a sub-specification from a given specification so that if the sub-specification satisfies a given verified formula, then so does the whole specification. We also show that functional requirements for the microcomputer software can be translated into verified formulas for an example specification.