モデル検査による設計検証と整合テスト
スポンサーリンク
概要
- 論文の詳細を見る
モデル検査は,扱える状態数の限界などから,実装よりは状態数が少い設計モデルの検証に適していると言われている.一方で,検証した設計モデルに基づいて実装する際,設計検証で保証した性質は,実装後も成立しているべきである.そこで,我々は,設計モデルと実装が整合していることを保証する手法について研究を行っている.ここでの整合性とは,設計モデルにおいてモデル検査により保証した性質が,実装においても成立することである.この整合性が成立することを,従来から研究されている整合テスト,特に,Automata-Theoretic Conformance Test の枠組を拡張してテストすることを試みる.
- 一般社団法人情報処理学会の論文
- 2009-07-17
著者
関連論文
- 組込みシステムシンポジウム2006実施報告(シンポジウム/ワークショップ実施報告)
- 組込みシステムシンポジウム2006実施報告(シンポジウム/ワークショップ実施報告)
- ウインターワークショップ2008・イン・道後開催報告
- プロジェクト紹介 : 高信頼組込み用オブジェクト指向設計技術(組込み・アスペクト指向)
- 1L-2 モデル検査によるリアルタイムオペレーティングシステムの検証実験(リーディングプロジェクト e-society:高信頼性組み込みソフトウェア(1),一般セッション,リーディングプロジェクト e-society)
- 2.形式的手法による高信頼性組み込みソフトウェア開発(高信頼性組み込みソフトウェア開発-最新技術動向と取り組み-)
- オブジェクト指向分析モデルにおけるデータフローの形式化と解析手法
- 第11回ソフトウェアプロダクトライン国際会議(SPLC2007)参加報告(ソフトウェア評価/プロダクトライン)
- ウインターワークショップ2008・イン・道後開催報告
- Alloyを用いた構成変更支援ツールと適用実験
- モデル検査による設計検証と整合テスト
- 「ウィンターワークショップ2007・イン・那覇」開催報告(シンポジウム/ワークショップ実施報告)
- 「ウィンターワークショップ2007・イン・那覇」開催報告(シンポジウム/ワークショップ実施報告)
- 編集にあたって(高信頼性組み込みソフトウェア開発-最新技術動向と取り組み-)
- コラボレーションに基づくオブジェクト指向モデルの検証(システム検証の科学技術)
- ウィンターワークショップ・イン・石垣島参加報告(会議報告)
- 編集にあたって(組み込みソフトウェア開発技術)
- 状態遷移図の段階的構築のための論理的基盤
- (形式的仕様)振舞い近似手法を用いたステートチャートに対する不変性の検証(オブジェクト指向技術)
- ウィンターワークショップin神戸報告
- Alloy を用いた構成変更支援ツールと適用実験
- 並行オブジェクトから並行処理列への変換法(ディペンダブルソフトウェア)
- オブジェクト指向方法論のための検証フレームワークに関する研究
- 定理証明技術のオブジェクト指向分析への適用
- オブジェクト指向分析モデルの検証と公理系の提案
- 並行オブジェクトモデルから並行スレッドモデルへの変換法
- APSEC2001参加報告
- 組み込みシステム設計における並行正規表現を用いたスレッド抽出法の適用
- 定理証明システムHOLにおけるオブジェクト指向理論の構築
- 組み込みシステムの動向
- 並行動作するオブジェクトからの処理列の抽出法
- 並行動作するオブジェクトからの処理列の抽出法
- オブジェクト指向組み込みシステム開発のためのSES-Basedアプローチ
- 形式的オブジェクト指向分析モデルFO∀Mの構築法とその支援環境
- オブジェクト指向方法論のための形式的モデルの検証
- オブジェクト指向方法論のための形式的モデル
- モデル検査ツールにより出力された反例に基づく誤り特定に関する研究