6L-7
リアクティブシステム仕様の実現不能判定器の高速化
○閨 芳紀，吉浦紀晃（埼玉大）
高い信頼性の求められるリアクティブシステムを開発するためには
形式的手法による検証が有効である．特に仕様の段階での自動検証は
開発コスト削減にも非常に効果的である．
そのリアクティブシステムの仕様が満たすべき性質の一つに実現可能性がある．
この性質を満たすことを検証するために，タブローと推論規則を用いた
実現不能性判定手続きの提案がされ，これに基づく実現不能判定器の
作成が行われた．しかしながら，この判定器では判定能力，速度共に
不十分で判定できない仕様が存在する．そこで，本研究では
より判定能力，速度に優れた実現不能判定器の開発を行う．