Formal Verification in a First-Order Extension of Modal μ-calculus
スポンサーリンク
概要
- 論文の詳細を見る
Formal verification is frequently based on modal μ-calculus and its fragments. However, the number of systems and verification properties which cannot be formalized in modal μ-calculus has been increasing as they become complicated. In this paper, we present a first-order extension of modal μ-calculus in order to formalize various such systems and verification properties. We also give an axiomatization of the logic. It is necessarily incomplete for the logic because the set of all valid formulas is not recursively enumerable. Finally, in order to demonstrate that our axiomatization is practical for verification, we formalize a system and mutual exclusion for unboundedly many processes in our first-order extension, and then verify that the system satisfies the property in our axiomatization.
- 日本ソフトウェア科学会の論文
日本ソフトウェア科学会 | 論文
- LCDと透明弾性体の光弾性を用いたユーザインタフェース (特集 インタラクティブシステムとソフトウェア)
- Bluetoothによる位置検出
- COINSにおけるSIMD並列化(最新コンパイラ技術とCOINSによる実践)
- データ型を考慮した軽量なXML文書処理系の自動生成(ソフトウェア開発を支援する基盤技術)
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)