An Efficient Method for Verification of Reactive System Specifications in Temporal Logic

DOI Web Site 17 References

Bibliographic Information

Other Title
  • 時間論理によるリアクティブシステム仕様の検証の効率化
  • ジカン ロンリ ニ ヨル リアクティブ システム シヨウ ノ ケンショウ ノ コウリツカ

Search this article

Abstract

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

Journal

  • Computer Software

    Computer Software 20 (3), 242-265, 2003

    Japan Society for Software Science and Technology

References(17)*help

See more

Details 詳細情報について

Report a problem

Back to top