UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
スポンサーリンク
概要
- 論文の詳細を見る
近年,情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている.実時間システムのモデル検査では,モデルの状態数が状態変数やクロック変数に対して指数的に増加し,スケーラビリティに厳しい制限が生じる.本稿では,時間モデル検査ツールであるUPPAALで用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する.モデル抽象化技法はこのスケーラビリティ改善のための主要な手法として注目を浴びている.本手法では,Clarkeらが提案した反例に基づいた抽象化改良ループCEGARを適用しており,抽象化から検査までの全ての工程を自動的に行うことが可能である.また,反例によるモデルの再抽象化においては時間オートマトンの検証で用いられるデータ構造DBMを活用する工夫を行なっている.
- 2007-07-26
著者
関連論文
- コードクローン検出とその関連技術(ソフトウェア工学)
- グラフマイニングアルゴリズムを用いたギャップを含むコードクローン情報の生成 (画像符号化・映像メディア処理レター特集)
- クラス階層構造を利用したコードクローン集約支援手法の改良(研究速報)
- グラフマイニングアルゴリズムを用いたギャップを含むコードクローン情報の生成(ソフトウェア工学)
- 類似性に基づく工数予測における適切でない予測プロジェクトの判別の試み
- Strutsフレームワークにおけるメタモデルを用いた追跡可能性実現手法の提案(アスペクト指向・Web)
- アスペクトマイニングを自動的に行うツールの提案
- アスペクト指向プログラムのデバッグ支援環境 : プログラムスライスとコールグラフの利用(オブジェクト指向とWeb技術)
- アスペクトを用いた表明の記述(開発支援(学生セッション))
- アスペクト指向プログラミングのプログラムスライス計算への応用(テスト技法・保守技術)
- アスペクト指向プログラムに対するプログラムスライシング
- D-3-4 アスペクト指向プログラミングの動的プログラムスライスへの応用
- 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
- メタモデルに基づくトレーサビリティ技術の提案
- D-3-9 UMLで記述された設計仕様書からのファンクションポイント計測手法
- 確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
- UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
- SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
- UML/OCLに記述された時間QoSの階層的検証手法の提案
- 確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
- SPINによるStrutsアプリケーションの動作検証を目的としたモデル生成手法の提案
- 問題の早期発見・改善を支援するインプロセスプロジェクト管理手法の実プロジェクトへの適用(ソフトウェア工学)
- 問題の早期発見・改善を支援するインプロセスプロジェクト管理手法の実プロジェクトへの適用
- 在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
- プログラム依存グラフを用いたコードクローン検出法の改善と評価
- D-13-5 新規開発者のソフトウェア理解を目的としたプログラム依存グラフ可視化手法の提案(D-13.知能ソフトウェア工学,一般セッション)
- 時間システムを対象とした到達可能性解析の高速化手法の提案
- 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
- OCLのJMLへの変換ツールの実装と評価
- OCLのJMLへの変換ツールの実装について
- 実時間システムを対象としたCEGARによる抽象洗練の並列化手法
- Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
- B-001 Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール(ソフトウェア,一般論文)
- JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証
- 制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,フォーマルアプローチ論文)
- Daikonの限定利用によるJavaメソッドの事後条件の自動導出
- UMLモデルに対するXPathとXMI-differenceを用いた不整合検出と解消
- 影響波及解析を利用した保守作業の労力見積りに用いるメトリックスの提案(ソフトウェア工学)
- 保守請負時を対象とした労力見積りのためのメトリクスの提案
- 大規模ソースコード集合を対象とした類似関数集合群の抽出
- プログラム実行履歴を用いたトランザクションファンクション抽出手法
- 動作オブジェクト群の変化に着目したオブジェクト指向プログラムの実行履歴分割手法
- D-3-5 協調動作するオブジェクト群に着目したJavaプログラムの実行履歴分割手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- ユースケースポイント計測におけるアクタとユースケースの自動分類の試みと支援ツールの試作(ソフトウェア工学)
- ソースコードからのファンクションポイント計測とその適用
- 多言語対応メトリックス計測プラグイン開発基盤MASUの開発(ソフトウェア工学)
- B-025 実プロジェクトデータからのソフトウェアタグ作成とその分析(ソフトウェア,一般論文)
- 事故前提社会に向けたユーザ・ベンダ間での開発データ共有 第2回 : −ソフトウェアタグ規格とソフトウェアタグ支援ツール−
- ユーザ視点に立ったソフトウェア開発データ活用技術の提案(解析・検証(一般セッション))
- Fault-proneモジュール判別におけるテスト工数割当てとソフトウェア信頼性のモデル化
- コードクローン検索による類似不具合検出の実証的評価(ソフトウェア工学)
- 利用実績に基づくソフトウェア部品重要度評価システム(ソフトウェア工学)
- ソースコード間の関係を用いた再利用性評価手法の提案
- 識別子の共起関係に基づく類似コード検索法の提案と欠陥検出への適用
- コードクローン検出ツールの差分情報を用いた不具合検出手法の提案と評価
- 1ZK-5 複数のコードクローン検出ツールによって検出されるコードクローンの差異を用いた不具合検出手法(リーディングプロジェクト e-society:コードクローン検出によるソフトウェア開発技術,一般セッション,リーディングプロジェクト e-society)
- D-13-6 重複コードと非重複コードに加えられる修正の頻度の比較 : 複数の検出ツールを用いた評価(D-13.知能ソフトウェア工学,一般セッション)
- D-3-2 複数の手法による予測結果が比較可能な工数予測ツールの開発(D-3.ソフトウェアサイエンス,一般セッション)
- 重複コードと非重複コードにおける修正頻度の比較
- RB-005 変数使用に着目したFault-Proneメソッド特定手法の提案と評価(ソフトウェア,査読付き論文)
- RB-004 メトリクス値の変遷を用いたFault-Proneモジュール特定手法の改良(ソフトウェア,査読付き論文)
- イベントトレース図に基づく要求仕様書からのファンクションポイント計測手法
- 5ZC-8 要求仕様書からのファンクションポイント計測ツールの改良 : 要求分析ツールREQUARIOで作成された要求仕様書を対象として
- 要求仕様書に対するファンクションポイント計測ツールの試作と評価
- 要求仕様書に対するファンクションポイント計測ツールの試作
- Javaソフトウェア部品検索システムSPARS-J(ソフトウェア工学)
- Javaを対象としたソフトウェア部品検索システムSPARS-Jの実験的評価
- Javaソフトウェア部品解析・検索システムSPARS-Jの構築
- Javaソフトウェア部品解析・検索システムSPARS-Jの構築
- Java ソフトウェア部品解析・検索システム SPARS-J の構築
- 利用頻度に基づくソフトウェア部品の解析・検索システムの提案
- 都市部における無線端末の移動特性を利用した情報共有方式(ユビキタス・モバイルアプリケーション,次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- 安定性の高い経路を構築する車車間ルーティングプロトコル(ITS,マルチメディア,分散,協調とモバイル(DICOMO2005))
- 安定性の高い経路を構築する車車間ルーティングプロトコルGVGridの性能評価(アドホックネートワーク(2))
- 安定性の高い経路を構築する車車間ルーティングプロトコルGVGridの性能評価(アドホックネートワーク(2))
- ファンクションポイント法を応用した早期見積技法の提案とそのシステム化(ソフトウェア工学)
- APIの使用に伴うコードクローンの特徴分析(ソースコード分析と可視化)
- APIの使用に伴うコードクローンの特徴分析(ソースコード分析と可視化)
- 画面遷移とデータベース処理を考慮したトランザクションファンクション識別手法の詳細化と実装
- モデル指向開発環境の提案(一般,学生セッション,一般)
- コードクローンを対象としたリファクタリングの有効性に関する調査
- ソフトウェア機能規模の自動計測の試み
- JAVAプログラムからのファンクションポイント計測に関する一考察
- ノードの移動フローを考慮したMANET上での情報共有方式とその評価(セッション8:データマネージメント)
- ノードの移動フローを考慮したMANET上での情報共有方式とその評価(セッション8:データマネージメント)
- Fault-Proneモジュール予測へのコードクローン情報の適用(研究速報)
- 教育環境におけるエラーデータ収集ツールの試作
- フォールト位置特定におけるプログラムスライスの実験的評価
- 移動端末間マルチホップ通信を用いた広告配信モデルの提案(MBL3:無線マルチホップ通信)
- 移動端末間マルチホップ通信を用いた広告配信モデルの提案(MBL3:無線マルチホップ通信)
- プログラム依存グラフを用いたTemplate Methodパターン適用によるコードクローン集約支援
- 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法
- プログラム変更支援を目的としたコードクローン情報付加ツールの実装と評価
- アドホック通信を用いた移動ノードの密度推定法(アドホックネットワーク1)
- 位置情報ルーティングによる車車間オーバレイネットワークの検討(交通における計測・一般)
- 位置情報ルーティングによる車車間オーバレイネットワークの検討
- 位置情報ルーティングによる車車間オーバレイネットワークの検討(交通における計測・一般)
- 修正頻度の比較に基づくソフトウェア修正作業量に対する重複コードの影響に関する調査
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (知能ソフトウェア工学)
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (ソフトウェアサイエンス)