記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案
スポンサーリンク
概要
- 論文の詳細を見る
高度な信頼性を要求されるハードウェア, ソフトウェアシステムの開発においては, システムが耐故障性を満たすことを形式的に証明することが必要とされている.本論文では, システムが耐故障性を満たしているか否かをモデル検査を用いて自動検証する手法の提案を行う.検証そのものには記号モデル検査をサポートするSMV(Symbolic Model Verifier)と呼ばれるツールを用いる.SMVはハードウェアシステムの検証のために開発され広く用いられており, ソフトウェアシステムの検証に用いられている例は少ない.ここでは, システムがガード付きコマンドによるプログラムでモデル化されていることを仮定して, そのモデルをSMVの入力言語によって表現する.そこで, まずそのモデルに基づいてシステムの記述を行うための言語を定義する.次に, その入力言語に従って記述されたシステムからSMV言語による記述へ変換するための手順を提案する.また, 文献から引用した例に対して提案法を適用した結果についても報告する.
- 社団法人電子情報通信学会の論文
- 2001-01-15
著者
-
菊野 亨
大阪大学 大学院基礎工学研究科 情報数理系専攻
-
横川 智教
岡山県立大学情報工学部情報システム工学科
-
菊野 亨
大阪大学 基礎工学部
-
横川 智教
大阪大学 大学院基礎工学研究科 情報数理系専攻
-
土屋 達弘
大阪大学 大学院基礎工学研究科 情報数理系専攻
関連論文
- ラウンドモデルからの変換による非同期コンセンサスアルゴリズムの導出(ネットワーク環境でのディペンダビリティ)
- 大学院情報系学生に対する技術者倫理教育(技術者倫理・情報倫理教育の現状と課題,及び一般)
- 3状態相互排他アルゴリズムの安定時間の下限について
- 非構造化オーバーレイネットワーク構築におけるメトロポリス法を用いたアルゴリズムの評価(ディペンダブルコンピュータシステムとセキュリティ技術及び一般)
- ペアワイズテスト : ソフトウェアテストの効率化を求めて
- Stochastic Timed Petri Net でモデル化した大規模論理回路の性能評価ツール
- リングセグメント型Globally Asynchronous Locally Synchronous Systemの構成法(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- モデル検査ツールUPPAALを用いたGALSシステムの形式的検証(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- マルチエージェントを用いた無中断予備VP設定方式
- 5 組込みシステムにおけるソフトウェアプロダクトラインの導入(ソフトウェア再利用の新しい波-広がりを見せるプロダクトライン型ソフトウェア開発-)
- Analyzerの簡単化 (情報科学の数学的理論)
- 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証(設計支援)
- 有界モデル検査を用いた複数UML図の形式的検証
- D-3-3 有界モデル検査を用いた複数UML図の検証に関する検討(D-3.ソフトウェアサイエンス,一般講演)
- Globally Asynchronous Locally Synchronous Systemの性能評価に関する一検討(上流設計技術(2),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 射影変換の高速化に関する一検討(演算回路/専用回路,システムオンシリコン設計技術並びにこれを活用したVLSI)
- K_067 透視化機能をもつマルチウィンドウシステムの高解像度化(K分野:ヒューマンコミュニケーション&インタラクション)
- B_003 シーケンス図と状態遷移図で記述されたUMLモデルを対象としたモデル検査による形式的検証(B分野:ソフトウェア)
- D-11-97 漸化式表現による再構成型幾何学変換器(D-11.画像工学D(画像処理・計測),一般講演)
- D-11-64 多眼カメラによるモザイク動画像生成に関する研究(D-11.画像工学D(画像処理・計測),一般講演)
- D-10-1 モデル検査手法を用いたUML図の検証(D-10.ディペンダブルコンピューティング,一般講演)
- C-024 ウィンドウの透視化と輝度低下機能を持つマルチウィンドウシステムの評価(C分野:アーキテクチャ・ハードウェア)
- D-11-69 射影変換を対象としたDRAM-SRAM間画像転送法(D-11. 画像工学B(画像デバイス・装置), 情報・システム2)
- D-11-27 RISC命令の並列実行機能を有する画像処理用DSP(D-11. 画像工学A(画像基礎・符号化), 情報・システム2)
- C-019 操作対象ウィンドウの透視化機能を持つマルチウィンドウシステム(C.アーキテクチャ・ハードウェア)
- モデル検査入門
- モデル検査を用いたコンセンサスアルゴリズムの合意性検証(ネットワーク環境でのディペンダビリティ)
- Interpolantを利用したモデル検査による機能競合の検証(ネットワーク環境でのディペンダビリティ)
- 耐故障分散アルゴリズムに対するPROMELAモデルの生成(ディペンダブルコンピューティングシステム及び一般)
- モデル検査器NuSMVを利用したテストケース自動生成(テスト・高信頼,組込技術とネットワークに関するワークショップETNET2008)
- ホームネットワークシステムにおける連携サービスのモデル検査による検証
- モデル検査による分散システムにおける合意アルゴリズムの安全性の検証(ディペンダブルソフトウェアとネットワーク及び一般)
- ホームネットワークシステムにおけるサービス競合の分類と解消について
- ソフトウェアメトリクスのデータマイニングによる障害発生要因特定
- 非構造化オーバーレイネットワーク構築におけるメトロポリス法を用いたアルゴリズムの評価(ディペンダブルコンピュータシステムとセキュリティ技術及び一般)
- 製品リリース履歴における論理的結合集合に基づいた横断フィーチャ分析法
- メソッド呼び出しに関する不具合修正での変更作業の分析
- ソフトウェアプロジェクト予測に用いるメトリクスの削減
- 複数の部分木の置換を許した属性木に対する属性評価アルゴリズムの提案
- ア***ロセッサの再構成に関するプロセッサ割当問題について
- プログラム仕様に用いる自然語処理のための語句の意味定義
- ベイズ識別器による不具合予測のための相関ルールマイニングを用いたメトリクス絞り込み
- ソフトウェア開発データに対する相関ルールマイニングを利用した不具合増加要因の調査
- ソフトウェアプロジェクト診断のためのチェックリスト導出(レビュー,品質(学生セッション))
- 企業横断的データからのプロジェクト改善案の相関ルールマイニングによる抽出
- 相関ルールマイニングによる企業横断データにおける不具合工数密度の分析
- 相関ルールマイニングの適用によるソフトウェア生産性の決定要因の分析(学生セッション C_開発プロセス)
- UseCASEを利用したソフトウェアフォールトに対するSS-FTAの提案
- ジャクソンシステム開発法の代数的言語による記述の試み
- GPUを用いた状態可到達性解析の高速化(ネットワーク環境でのディペンダビリティ,及び一般)
- 欠損を含むプロジェクトデータからのプロジェクト成否予測のための特徴抽出
- Webアプリケーションの脆弱性検出を目的とした自動テストツールの性能評価(ネットワーク環境でのディペンダビリティ,及び一般)
- メソッドに対するコメント文記述の変更履歴とメソッドの不具合との関係に関する実証的考察 (ソフトウェアサイエンス)
- フォールトプローンモジュール検出手法間の精度比較 : Fault-pronenessフィルタリングとロジスティック回帰
- ソースコード中に含まれる不具合トークンをテキスト分類に基づいて推定するツールの試作と評価
- ソースコード中に含まれる不具合トークンをテキスト分類に基づいて推定するツールの試作と評価
- Fault-Proneフィルタリング--不具合を含むモジュールのスパムフィルタを利用した予測手法
- 相関ルールマイニングによるソフトウェア開発プロジェクト中のリスク要因の分析(推薦論文・ソフトウェア工学の基礎)
- オーバーサンプリングを用いた効率的品質管理のための変数選択手法
- オーバーサンプリングを用いた効率的品質管理のための変数選択手法
- ベイズ識別器による混乱予測に基づくソフトウェアプロジェクト管理支援ツールの試作(学生セッション C_開発プロセス)
- 汎用テキスト分類フィルタを利用した不具合を含むソースコードの予測
- 相関ルールマイニングを用いた混乱プロジェクトの特徴分析ランダムサンプリングデータへの適用
- ピアの近接性を考慮したスキップグラフの構築
- Globally Asynchronous Locally Synchronous Systemの性能評価に関する一検討(上流設計技術(2),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 射影変換の高速化に関する一検討(演算回路/専用回路,システムオンシリコン設計技術並びにこれを活用したVLSI)
- 1-2 スパムフィルタリングに基づくフォールトプローンモジュール検出器の開発(セッション1「プロジェクト管理・ソフト」)
- 5B-2 品質定量指標のための異なるプログラミング言語間での規模の比較の試み(プロジェクトの定量的管理,一般セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- ゴシップ型ブロードキャストの高信頼化のための適応的再送手法の提案(ネットワーク,SWoPP2006)
- スケールフリーネットワークに対するゴシップアルゴリズムの高信頼化手法の提案(データ工学, ディペンダビリティ, 一般)
- スケールフリーネットワークに対するゴシップアルゴリズムの高信頼化手法の提案(データ工学, ディペンダビリティ, 一般)
- 記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案
- ソフトウェア開発プロジェクトのリアルタイム管理を目的とした支援システム(ソフトウェア開発環境・開発支援システム, システム開発論文)
- ピアの近接性を考慮したスキップグラフの構築
- マルチエージェントを用いた無中断予備VP設定方式
- データベースカーネルの設計と仕様の代数的記述
- C++プログラムの複雑度評価尺度の提案とその実験的評価
- ソフトウェア開発における不具合発見履歴と最終品質の関係に対する統計的分析
- レビュー作業の質に着目したソフトウェア最終品質の推定
- ソフトウェア開発プロジェクトにおける開発計画の分析 : 品質, 生産性との関連性
- 時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用
- LTSAを用いたシーケンス図の詳細化関係の検証
- 無線モバイルマイクロセンサーネットワークにおける自己組織的センサー配置手法の提案
- 非決定性フィーチャーインタラクションに対するP-インバリアントに基づく検出法の実験的評価
- タブーサーチを用いた臨床実習スケジューリングの自動化
- AS-1-2 GALSシステムを対象としたペトリネットシミュレーションにおけるアービタのモデル化(AS-1.モデリングとシミュレーションの最新動向,シンポジウムセッション)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- GPGPUを用いた透視化マルチウィンドウの一高速合成手法(視覚とIMQ一般)
- Globally Asynchronous Locally Synchronous Systemにおける非同期バスの一構成法(計算機システム)
- B-027 時間ペトリネットでモデル化されたGALSシステムを対象としたUPPAALによる自動検証手法(ソフトウェアサイエンス,B分野:ソフトウェア)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- C-016 多様な資源を対象とした多資源非同期式アービタの一構成(システム設計,C分野:ハードウェア・アーキテクチャ)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- 状態マシン図を用いたスマートフォンアプリのモデル化
- 状態マシン図を用いたスマートフォンアプリのモデル化