時間論理によるリアクティブシステム仕様の検証の効率化

書誌事項

タイトル別名
  • An Efficient Method for Verification of Reactive System Specifications in Temporal Logic
  • ジカン ロンリ ニ ヨル リアクティブ システム シヨウ ノ ケンショウ ノ コウリツカ

この論文をさがす

抄録

リアクティブシステムでは,停止せずに正しい応答動作をしつづけることが,システムセキュリティ上の最重要課題である.応答動作の仕様が多岐にわたり複雑化した場合,いかなる要求に対しても仕様を満たしながら応答しつづけることが原理的に不可能になる場合がある.この原因を解析するため,充足可能性や段階的充足可能性,強充足可能性など,仕様を満たすシステムが存在するための必要条件が,その判定アルゴリズムとともに提案されている.しかし既存のアルゴリズムでは,現実的な応用を考えた場合,その計算量が問題となっている.本稿では,仕様の充足可能性及び段階的充足可能性手続きを効率化する手法を提案し,その効果を実験によって確かめたことを報告する.

収録刊行物

参考文献 (17)*注記

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ