設計誤り検出のためのモデル検査を用いたソフトウェア解析システムの開発

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14019055
• Research Institution: Osaka University
• Principal Investigator: 土屋 達弘 大阪大学, 大学院・情報科学研究科, 助教授 (30283740)
• Keywords: 記号モデル検査 / 充足可能性判定 / 設計誤り / 機能競合 / 並行性

Research Abstract

信頼性の高い情報システムを実現するためには,設計誤りを開発のできるだけ早期の段階で検出することが非常に重要となる.そのための手法として,システム上で起こりうる状態を網羅的に調べるモデル検査と呼ばれる方法が知られている.本課題では,近年になって開発されたモデル検査手法である限定モデル検査(Bounded Model Checking)を,非同期的な並行動作を有するソフトウェアシステムに適用するための研究を行った.
限定モデル検査では,遷移関係を表現した論理関数からシステムの誤った振舞いを表現する一つの論理式を構成する.この論理式が充足可能であればシステムに設計誤りがあることを結論できる.しかし,従来の手法では,ソフトウェアシステムを対象とした場合,この論理式が非常に大きくなってしまい,効率良く検証が行えなかった.
本研究では,平成13年度に開発した新しい論理式構成手法を改良し,1)これまで扱うことのできなかった種類の誤りの検出,及び,2)検証効率の向上,を実現した.
1については,これまで安全性に関する誤りのみ検出可能であったものを,活性に関する性質についても可能にした.2については,論理式の生成前にシステムの動作規則の依存関係を予め考慮するような前処理を行うことで実現した.
ペトリネットと通信電話サービスを具体的な検査対象として,これらの提案手法を実装した.実験の結果,従来の限定モデル検査や,他のモデル検査手法に比べ,非常に効率の良く設計誤りが検出できることが分かった.

Research Products

• [Publications] 田中崇浩, 土屋達弘, 菊野亨: "充足可能性判定を用いたモデル検査ツールの実装"電子情報通信学会技術報告. 102・27. 1-6 (2002)
• [Publications] 濱田貴之, 土屋達弘, 中村匡秀, 菊野亨: "Detecting Feature Interactions in Telecommunication Systems by Symbolic Model Checking"Lecture Notes in Computer Science (Proc. of ICOIN 16). 2343. 641-651 (2002)
• [Publications] 土屋達弘, 中村匡秀, 菊野亨: "Symbolic Approaches to Feature Interaction Detection"Fastabstract : IEEE Conference on Dependable Systems and Networks. B46-B47 (2002)
• [Publications] 土屋達弘, 中村匡秀, 菊野亨: "Detecting Feature Interactions in Telecommunication Services with a SAT Solver"Proc. of 2002 Pacific Rim International Symposium on Dependable Computing (PRDC'02). 131-134 (2002)
• [Publications] 土屋達弘, 菊野亨: "非同期並行システムに対するSATに基づくモデル検査"電子情報通信学会技術研究報告. 102・378. 31-36 (2002)
• [Publications] 市原浩司, 土屋達弘, 菊野亨: "ペトリネットに対するSATを利用したモデル検査の効率化"電子情報通信学会技術研究報告. 102・616. 7-11 (2003)