5L-5
モデル検査における健全性を満たす変数抽象化方法の提案
○加藤友章，中道 上，青山幹雄（南山大）
自動車等の組込みソフトウェアは高信頼性を求められるが，ソフトウェアの大規模化，複雑化から，テストのみでは高信頼性の確保が困難である．そのため，モデル検査が注目されているが，状態爆発問題からモデルの抽象化が必要である．
本稿では，組込みソフトウェアがセンサから得た速度，温度等の多数の変数を扱うことが多いことに着目し，変数の抽象化を行う．さらに，抽象化前後のモデルの健全性を保持するための条件を導入する．その条件により命題に基づいて変数を分割，抽象化することにより，健全性を保持したモデルの変数を抽象化する方法を提案する．提案方法をクルーズコントロール制御へ適用し，検証時間，反例を抽象化前後で比較し，妥当性を評価する．