An Efficient Method for Verification of Reactive System Specifications in Temporal Logic
-
- AOSHIMA Takenobu
- Matsushita Electric Industrial Co., Ltd.
-
- YONEZAKI Naoki
- Tokyo Institute of Technology
Bibliographic Information
- Other Title
-
- 時間論理によるリアクティブシステム仕様の検証の効率化
- ジカン ロンリ ニ ヨル リアクティブ システム シヨウ ノ ケンショウ ノ コウリツカ
Search this article
Description
リアクティブシステムでは,停止せずに正しい応答動作をしつづけることが,システムセキュリティ上の最重要課題である.応答動作の仕様が多岐にわたり複雑化した場合,いかなる要求に対しても仕様を満たしながら応答しつづけることが原理的に不可能になる場合がある.この原因を解析するため,充足可能性や段階的充足可能性,強充足可能性など,仕様を満たすシステムが存在するための必要条件が,その判定アルゴリズムとともに提案されている.しかし既存のアルゴリズムでは,現実的な応用を考えた場合,その計算量が問題となっている.本稿では,仕様の充足可能性及び段階的充足可能性手続きを効率化する手法を提案し,その効果を実験によって確かめたことを報告する.
Journal
-
- Computer Software
-
Computer Software 20 (3), 242-265, 2003
Japan Society for Software Science and Technology
- Tweet
Details 詳細情報について
-
- CRID
- 1390282679715254272
-
- NII Article ID
- 110003743115
-
- NII Book ID
- AN10075819
-
- NDL BIB ID
- 6650819
-
- ISSN
- 02896540
-
- Text Lang
- ja
-
- Data Source
-
- JaLC
- NDL
- CiNii Articles
-
- Abstract License Flag
- Disallowed