モデル検査ツールにより出力された反例に基づく誤り特定に関する研究
スポンサーリンク
概要
- 論文の詳細を見る
モデル検査ツールにより出力される反例の自動解析において,既存研究では誤りの特定までは至っていないが,本研究では,並行計算によくあるrace conditions問題を対象として取り上げ,race conditions問題の特徴を付加情報としてモデルの誤り自動特定法を提案した.また,提案手法に従って反例解析ツールを実装して,race conditions問題のモデル例に適用し,提案手法の評価を行った.
- 2012-07-12
著者
関連論文
- 組込みシステムシンポジウム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の構築法とその支援環境
- オブジェクト指向方法論のための形式的モデルの検証
- オブジェクト指向方法論のための形式的モデル
- モデル検査ツールにより出力された反例に基づく誤り特定に関する研究