CSP-Prover:プロセス代数CSPのための定理証明器
スポンサーリンク
概要
- 論文の詳細を見る
我々は汎用定理証明器Isabelle上にプロセス代数CSPの理論を実装し, CSPのための証明支援ツールCSP-Proverを開発している.CSP-Proverには, 完備距離空間と完備半順序の理論が実装されており, そこでBanachの不動点定理とTarskiの不動点定理が証明されている.これらはCSPにおいて再帰動作を解析するために使われる重要な定理である.現在のCSP-Proverでは, プロセス(動作)の意味は安定失敗モデルFを基に定義されており, その再帰動作は主にBanachの不動点定理によって解析されている.さらに, CSPの規則も多数証明されており, そのCSPの規則を基にプロセスの詳細化関係を半自動的に検証するコマンドも用意されている.すなわち, CSP-ProverはCSPの新しいモデルや規則の証明のような研究を支援するだけでなく, 実際の並行システムの検証支援にも有効である.特に無限の状態を持つプロセスの詳細化関係を不動点帰納法等によって検証できる特長を持つ.本発表ではCSP-Proverについて説明するとともに, 実際の電子支払システムEP2と無限状態を持つ数学者の食事問題にCSP-Proverを適用してその有効性を実証する.
- 一般社団法人情報処理学会の論文
- 2005-08-15
著者
関連論文
- Promelaにおける割り込み制御処理の半自動モデル化 (コンカレント工学)
- Promelaにおける割り込み制御処理の半自動モデル化 (信号処理)
- Promelaにおける割り込み制御処理の半自動モデル化 (VLSI設計技術)
- Promelaにおける割り込み制御処理の半自動モデル化 (回路とシステム)
- 並行システムを解析するための逐次化と状態削減機能の実装--仕様の自動生成を目指して (信号処理)
- 並行システムを解析するための逐次化と状態削減機能の実装 : 仕様の自動生成を目指して(システムと信号処理及び一般)
- Promelaにおける割り込み制御処理の半自動モデル化(システムと信号処理及び一般)
- 並行システムを解析するための逐次化と状態削減機能の実装 : 仕様の自動生成を目指して(システムと信号処理及び一般)
- Promelaにおける割り込み制御処理の半自動モデル化(システムと信号処理及び一般)
- CAS2010-25 並行システムを解析するための逐次化と状態削減機能の実装 : 仕様の自動生成を目指して(システムと信号処理及び一般)
- CAS2010-24 Promelaにおける割り込み制御処理の半自動モデル化(システムと信号処理及び一般)
- 並行システムを解析するための逐次化と状態削減機能の実装 : 仕様の自動生成を目指して(システムと信号処理及び一般)
- Promelaにおける割り込み制御処理の半自動モデル化(システムと信号処理及び一般)
- Stepwise Synthesis of Partial Specifications preserving Strong $(\Omega_1,\Omega_2)$-Equivalence(Concurrency Theory and Applications '96)
- アクティブデータベースの動作解析のためのプロセス代数の開発
- プロセス代数によるプロセス生成機能をもつ並行システムの解析
- 準弱双模倣性をもとにした仕様の段階的合成方法
- 準弱双模倣性をもとにした仕様の段階的合成方法(並列・分散)
- グレイド付き空間プロセス代数による近似解析 ( ソフトウェア工学の基礎)
- 受信者数を考慮したブロードキャストシステムのためのプロセス代数 (ソフトウェア工学の基礎)
- プロセス代数CSPによるシーケンス図設計の詳細化と検証(組込みシステム,一般)
- 論理型オブジェクト指向データベースF-logicの実装と基本概念への考察
- タスクの順序に基づくビジネスプロセスの検証方法の提案(一般)
- CSP-Prover : スケーラブルな並行システムの検証のための証明器(エージェント)
- CSP-Prover:プロセス代数CSPのための定理証明器
- プロセス計算におけるセキュリティ
- エージェントの合成を検証するための非インターリービング時間付プロセス代数とプロセス論理
- 真の並行プロセス代数のための決定可能な局所プロセス論理
- 真の並行プロセス代数のためのプロセス論理における充足可能性の決定不能性
- 分散システムのためのプロセス論理の充足可能性判定ツール
- 論理的な仕様から分散システムを合成する方法の検討
- プロセス論理演算子をもつプロセス代数