事例研究:プリエンプティブな周期タスクからなる組込みソフトウェアのモデリング,仕様記述と有限モデル検査(ディペンダブルコンピューティング)
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,プリエンプティブな周期タスクからなる組込みソフトウェアのモデリング,仕様記述と有限モデル検査の事例研究を報告する.まず,Alurらのストップウォッチオートマトンを用いて,環境とOSを含めた組込みソフトウェア全体をモデリングする.ストップウォッチオートマトンを用いることで,タスクの詳細な動作をモデリング可能となり,排他制御の可否のような,スケジューラビリティ以上の検証も行うことができた.次に,作成されたモデルに対し,有限モデル検査を行う.そのモデル検査の制限時間には,全タスクの周期の最小公倍数と最長の周期の和を設定する.この工夫により,無限に動作を繰り返す,周期タスクからなるシステムの安全性を,有限の時間で検証できた.また,HYTECHにより,作成した組込みソフトウェアの有限モデル検査を行って,妥当な検証時間で検証できることを示した.
- 2010-11-01
著者
-
山根 智
金沢大学大学院自然科学研究科電子情報工学専攻
-
瀧内 新悟
金沢大学大学院自然科学研究科
-
山根 智
金沢大学自然科学研究科
-
山根 智
金沢大学自然科学研究科電子情報工学専攻
-
山根 智
金沢大学大学院自然科学研究科
-
山根 智
金沢大学工学部情報システム工学科
-
瀧内 新悟
金沢大学大学院自然科学研究科電子情報工学専攻
-
山根 智
金沢大学理工研究域電子情報学系
関連論文
- 確率時間ゲーム理論による組込みシステムのモデル化,仕様記述及び検証(ディペンダブルコンピューティング)
- コスト付き確率時間オートマトンの抽象化精錬を用いた到達可能性解析手法 (アルゴリズムと計算機科学の数理的基盤とその応用)
- 動的再構成可能プロセッサ向け仕様記述言語の開発と実問題の適用 (アルゴリズムと計算機科学の数理的基盤とその応用)
- 確率時間REGARによるPTCTLのサブクラスのモデル検査
- 確率ゲーム理論による組込みシステムのモデル化とモデル検査
- CPUと動的再構成可能プロセッサとの協調システムのモデル検査(ペトリネット,離散事象システム,一般)
- 組込みシステムのUML分析設計からタスク設計までの設計検証方法論(UML/開発方法論)
- 確率時間REGARの実装と評価 (知能ソフトウェア工学)
- 確率時間REGARの実装と評価 (ソフトウェアサイエンス)
- 並列動作する確率時間システムに対する拡張CEGAR(モデル化・仕様記述)
- 階層時間オートマトン群の並列動作の述語抽象化精錬検証手法(グラフ,ペトリネット,ニューラルネット,及び一般)
- UMLと時間オートマトンを用いたソフトリアルタイムシステムの設計解析手法(分析・設計技法)
- UMLと価値関数を用いたソフトリアルタイムシステムの設計検証手法(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- 確率時間ゲーム理論による組込みシステムのモデル化, 仕様記述及び検証 (理論計算機科学の深化と応用)
- 組込みシステム設計検証のためのゲーム理論(「エージェント基礎」及び一般)
- 確率時間ゲーム理論に基づくリアルタイム組込みシステム設計検証手法
- 事例研究:プリエンプティブな周期タスクからなる組込みソフトウェアのモデリング,仕様記述と有限モデル検査
- 空間の概念を持つコスト付き確率時間オートマトンの提案とセンサネットワークへの適用(ペトリネット,離散事象システム,一般)
- 確率時間CEGAR(研究会優秀論文賞,ペトリネット,離散事象システム,一般)
- 確率ゾーングラフを用いた確率時間強模倣関係による検証(ディペンダブルコンピューティング)
- 述語抽象化とその洗練による確率時間オートマトンの到達可能性解析手法(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- ストップウォッチオートマトンによるプリエンプティブスケジューリングの仕様記述と有界モデル検査 (理論計算機科学の深化 : 新たな計算世界観を求めて)
- 確率時間インターフェース理論による組込み型システムの設計手法(グラフ, ペトリ, ニューラルネット及び一般)
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法(検証/テストとデバッグ)
- 離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時同時相論理式の保存(設計手法)
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
- 離散確率分布を持つリアルタイムシステムの詳細化検証手法(検証/テストとデバッグ)
- 実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価
- 離散確率分布を持つリアルタイムシステムの詳細化検証手法
- 事例研究:プリエンプティブな周期タスクからなる組込みソフトウェアのモデリング,仕様記述と有限モデル検査(ディペンダブルコンピューティング)
- 東洋史研究のためのエージェントとサービス(「エージェント基礎」及び一般)
- コンポーネントウェアによる確率リアルタイムシステムの設計検証手法
- 確率ゲーム理論による組込みシステムのモデル化とモデル検査
- 確率時間REGARの実装と評価(一般セッション)
- 確率時間REGARの実装と評価(一般セッション,一般,フレッシャーズセッション)
- 動的リアルタイムCEGAR(一般セッション)
- 動的再構成可能プロセッサの離散シミュレータの開発(コンカレントシステム,離散事象システム及び一般)
- 確率時間REGARによるPTCTLのサブクラスのモデル検査
- 確率時間CEGAR (理論計算機科学の深化と応用)
- 階層時間オートマトン群の並列動作の述語抽象化精錬検証手法(グラフ,ペトリネット,ニューラルネット,及び一般)
- 空間の概念を持つコスト付き確率時間オートマトンの記号的検証手法(一般セッション)
- 空間の概念を持つコスト付き確率時間オートマトンの記号的検証手法(一般セッション,一般,フレッシャーズセッション)
- 動的リアルタイムCEGAR(一般セッション,一般,フレッシャーズセッション)
- 動的再構成可能組込みシステムのモデル化と仕様記述(モデル化・仕様記述)
- 確率時間強模倣検証アルゴリズムの実現
- 確率時間オートマトンの確率時間弱模倣検証理論(計算理論とアルゴリズムの新展開)
- 時間弱模倣検証に基づくリアルタイムソフトウェアの詳細化設計手法(ディペンダブルコンピューティング)
- 時間弱模倣関係と最悪応答時間に基づくリアルタイムソフトウェアの詳細化設計手法(2003年並列/分散/協調処理に関する「松江」サマーワークショップ(SWoPP松江2003))(DC-1高信頼化手法)
- 確率時間インターフェース理論による組込み型システムの設計手法(グラフ, ペトリ, ニューラルネット及び一般)
- 非線形ハイブリッドオートマトンの近似解析による到達可能性解析検証手法(グラフ,ペトリ,ニューラルネット及び一般)
- 非線形ハイブリッドオートマトンの近似解析による到達可能性解析検証手法(グラフ,ペトリ,ニューラルネット及び一般)
- 述語抽象化洗練を用いたリアルタイムプログラムの自動検証手法(計算機科学の理論とその応用)
- 述語抽象化とその精錬による確率線形ハイブリッドオートマトンの到達可能解析手法(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- 確率線形ハイブリッドオートマトンの記号的到達可能性解析手法(グラフ,ペトリ,ニューラルネット及び一般)
- 確率線形ハイブリッドオートマトンの記号的到達可能性解析手法(グラフ,ペトリ,ニューラルネット及び一般)
- 動的リアルタイムハイブリッド CEGAR による動的再構成可能組込みシステムの設計検証 (計算機科学とアルゴリズムの数理的基礎とその応用)
- 確率時間 WiGAR による PTCTL サブクラスのモデル検査 (計算機科学とアルゴリズムの数理的基礎とその応用)
- 確率時間オートマトンの確率時間強模倣検証器の開発(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- DLHAによるCPUとDRPの協調動作の組込みシステムのシステム仕様記述
- DLHAによるCPUとDRPの協調動作の組込みシステムのシステム仕様記述
- AS-4-3 制限付きストップウォッチオートマトンと時間オートマトンを用いた,プリエンプティブスケジューリングシステムのUML分析設計からタスク設計までの設計検証方法論(ソフトウェアのテストと検証,AS-4.組込みシステムの形式的手法,シンポジウム)
- 価値関数によるソフトリアルタイムシステムのスケジューラ自動合成手法(計算機科学の理論とその応用)
- ハイブリッドシステムのモジュールの仕様記述と検証の手法
- ハイブリッドオートマトンによるリアルタイムソフトウェアの仕様記述とスケジューラビリティ検証
- ハイブリッドモジュールの詳細化自動検証手法
- ハイブリッドシステムの構成的証明とその計算機実験
- リアルタイムシステムの形式的手法とその検証ツール(ソフトウェア紹介)
- 時間オートマトンによる Value-Density スケジューリングアルゴリズムの性能解析手法(計算理論とアルゴリズムの新展開)
- リアルタイムステートチャートによる形式的手法
- 時間オートマトンによるソフトリアルタイムシステムの性能解析手法(検証/テストとデバッグ)
- 確率時間CEGARの開発とその実証実験 (プログラミング Vol.5 No.2)
- 確率時間オートマトンの確率時間強模倣検証アルゴリズム (計算機科学基礎理論とその応用)
- 抽象化洗練を用いた時間確率システムに対する形式的検証手法 (アルゴリズムと計算理論の新展開)
- 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
- 確率線形ハイブリッドオートマトンの到達可能性検証
- 時間オートマトンによるソフトリアルタイムシステムのスケジューリング解析(スケジューリング, VLSI 設計とテスト及び一般)
- 動的組込みシステムの仕様記述言語の開発
- 組込みシステムを対象とした線形ハイブリッドオートマトンのモデル検査器の開発と検証