Event-Bで書かれたシステム要求仕様の妥当性検査
スポンサーリンク
概要
- 論文の詳細を見る
Event-Bの仕様構築過程では標準の証明条件による検証に加えて、振る舞い性質の確認を行う方法が必要となる。状態の変化列を表すトレースに対する時相的な性質を調べればよい。しかし、Event-Bの式言語は一般には算偽値が決定不能であり、トレース生成に必要な状態遷移関係の計算ができない。本稿では抽象化支援検証の考え方を採用し、Event-Bに述語抽象による過大近似を導入する方法を考察する。抽象化対象述語の選び方に関する指針を提案し、抽象化遷移の計算にRODINを用いる方法を報告する。
- 2010-07-29
著者
-
中島 震
特集編集委員
-
中島 震
国立情報学研究所:総合研究大学院大学
-
中島 震
国立情報学研究所 アーキテクチャ科学研究系:科学技術振興機構 Sorst
-
中島 震
情報・システム研究機構国立情報学研究所:科学技術振興機構さきがけ
-
中島 震
情報・システム研究機構 情報学研
-
中島 震
国立情報学研究所|総合研究大学院大学
-
中島 震
国立情報学研
-
中島 震
総合研究大学院大学|国立情報学研究所
関連論文
- Webアプリケーション・フィーチャのアスペクト隠蔽
- UMLとSimulinkのモデル変換手法の検討
- Event-Bデザインのモデル検査における抽象化(モデル表記・モデル検査)
- RBACモデルの形式検証と修正支援(形式手法(1)・言語(学生セッション))
- AOPによるWebアプリケーションの要求監視
- アスペクト概念を持つステートダイアグラムの提案(アスペクト指向)
- プロジェクト紹介 : 高信頼組込み用オブジェクト指向設計技術(組込み・アスペクト指向)
- 振る舞い仕様の実行時モニタリング
- 代数仕様言語Maudeを用いた制約オートマトンの実現(形式的手法)
- Cプログラム・モデル検査におけるDbC(一般セッション2:モデル検査とコデザイン)
- リアルタイム・コンポーネント向けの程良い形式手法
- 制約オートマトンを用いたソフトウェア・デザインの記述法
- 制約オートマトンに関するモデル検査法の実験
- UMLステートダイアグラムの亜種を用いた組み込みソフトウェア振舞い解析(分析・設計技法)
- プライオリティ概念のあるステートダイアグラムのモデル検査
- 状態遷移システムを用いたデザインのモデル検査
- 3 組み込みソフトウェアのモデル検査技術入門(組み込みソフトウェア開発技術)
- Webサービスにおける安全性とセキュリティの解析
- ジョインポイント写像によるドメイン特化AO機構の開発手法
- ポリシー規則と振る舞い仕様の分離への書き換え論理アプローチ(一般セッション)
- ポリシー規則と振る舞い仕様の分離への書き換え論理アプローチ(一般セッション,一般,フレッシャーズセッション)
- ユビキタスアプリケーション向け移動エージェントの相互運用
- コンテキストベース・プロダクトライン開発とVDM++の適用(ソフトウェアプロダクトライン開発,ソフトウェア工学の理論と実践)
- 検証モデリングの比較検討 : 組込みシステムの事例(組込みシステム,一般)
- Event-Bで書かれたシステム要求仕様の妥当性検査
- Event-Bデザインのモデル検査における抽象化(モデル表記・モデル検査)
- 特集「組込みシステム工学」の編集にあたって
- 移動エージェント相互運用の実現 : 基本アーキテクチャ
- 3S-4 移動エージェント相互運用の実現 : ディレクトリサーバ
- 3S-3 移動エージェント相互運用の実現 : インカネーションエージェントによる相互運用の実現
- 3S-2 移動エージェント相互運用の実現 : 基本アーキテクチャ
- 3S-1 移動エージェント相互運用の実現 : 背景と構想
- Webアプリケーション開発向けAOP機構の実装(Webアプリケーション(学生セッション))
- 特集「ソフトウェア開発を支援する基盤技術」の編集にあたって(ソフトウェア開発を支援する基盤技術)
- 仕様記述言語Zと証明環境Isabelle/HOL-Z(ソフトウェア紹介,先端ソフトウェアツール)
- Webサービスにおける安全性とセキュリティの解析
- リファクタリングの正しさのESC/Java2による形式検証
- 形式手法の潮流 : アーキテクチャへの関心(システム設計のための形式手法の基礎と応用)
- 制約概念を用いるソフトウェアデザイン
- Alloy : 自動解析可能なモデル規範形式仕様言語
- 有界モデル検査法を用いたCプログラムのモジュラー検証
- FODAフィーチャー・ダイアグラムの形式化と検査の自動化
- 有界モデル検査法を用いたモジュラー検証のテストケース生成による補完
- プログラム簡易検証ツールESC/Java2(ソフトウェア紹介,先端ソフトウェアツール)
- 先端ソフトウェアツール小特集(先端ソフトウェアツール)
- モデル検査法のソフトウェアデザイン検証への応用(新しいソフトウェアの実現,サイバー増大号)
- ソフトウェアモデル検査とテストケース生成の統合
- 有限Alloy記述の段階的な構築について
- 自己適応 Web アプリケーションシステム : 概念アーキテクチャと実現フレームワーク
- AP-1-1 モデリング、モデル、解析(AP-1.サイバーフィジカルシステムにおけるモデリング手法,パネルセッション,ソサイエティ企画)