モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般)
スポンサーリンク
概要
- 論文の詳細を見る
多種のシステムを低コストで短期間に開発しなければならない組込みソフトウェアなどの分野でもモデル検査手法のような設計検証技術が容易に使えるようになることに期待が高まっている.時間制約のあるシステムでは,動的な挙動をシーケンスチャートで定義し,ステートチャートでプロセスの静的な挙動を定義することが多い.性能モデル検査はプロセス毎のステートチャートと同等の時間オートマトンで定義された挙動を検証するものであるが検証したい性質を時相論理式で与える点が,設計者にとって利用の敷居を高くしている理由の1つである.本稿では,モデル検査ツールUPPAALを対象として,シーケンスチャートから検証したい性質を表現するオブザーバを機械的に生成する手法を提案し,通信プロトコルのアプリケーションに適用してオーバーヘッドの評価を行った.
- 社団法人電子情報通信学会の論文
- 2006-11-03
著者
-
深澤 良彰
早稲田大学大学院基幹理工学研究科:国立情報学研究所
-
長谷川 哲夫
株式会社 東芝 ソフトウェア技術センター
-
長谷川 哲夫
(株)東芝研究開発センター
-
長谷川 哲夫
株式会社東芝
-
長谷川 哲夫
株式会社 東芝:早稲田大学
-
長谷川 哲夫
早稲田大学
-
深澤 良彰
早稲田大学
-
長谷川 哲夫
(株)東芝
関連論文
- マルチエージェントシステムにおけるメタデータを用いた協調プロトコル合成手法(モデル/理論,ソフトウェアエージェントとその応用論文)
- Web画像に対する代替記述の適切性の評価手法(聴覚と福祉情報工学・一般)
- アスペクト指向技術の適用によるドメインフレームワークのモジュール性向上(オブジェクト指向とWeb技術)
- アスペクト指向の導入によるフレームワークの理解容易性の向上(組込みソフトウェア工学及び一般)
- アスペクト指向の導入によるフレームワークの理解容易性の向上
- ユーザの操作を基にしたユーザビリティ自動評価手法 (知能ソフトウェア工学)
- ループパーティショニングを用いたショートベクトル化技法
- ユーザ要求に対するパッケージソフトウェアの適合度導出手法
- 1Y-6 JavaFX Scriptによる動的コンテンツのアクセシビリティ向上手法(ユーザインタフェース,学生セッション,インタフェース)
- 1M-1 操作履歴を利用したユーザビリティ評価手法(ソフトウェア実装,学生セッション,ソフトウェア科学・工学)
- 携帯端末用Webページから通常端末用ページを構成する手法--Webページのモデル化とその評価 (ソフトウェアサイエンス)
- 適応エージェントのためのユビキタスコンピューティングミドルウェア(エージェント)
- 6Q-7 要求仕様とモデルの共通性・可変性分析によるソフトウェアプロダクトライン構築(要求定義,MDA,プロダクトライン,学生セッション,ソフトウェア科学・工学)
- 6N-4 レジスタ干渉グラフの分割による高速化手法に関する研究(数値計算とコンパイラ技術,学生セッション,アーキテクチャ)
- D-3-10 ガイドラインに則したGUIレイアウトの自動調整手法(D-3. ソフトウェアサイエンス,一般セッション)
- A-19-2 Webサイトの画像に対する代替テキスト記述の評価手法(A-19. 福祉情報工学,一般セッション)
- MDA体系に沿ったGUIモデル変換手法
- 非再試行型レジスタ割付けとその評価
- B-029 MDAモデル変換によるGUIプロトタイプ生成手法(B分野:ソフトウェア)
- 生存区間分割時に発生する偽干渉を避けるための同時コピー中間コードの利用(ARC-6 : ソフトウェア最適化,2007年並列/分散/協調処理に関する『旭川』サマー・ワークショップ(SWoPP旭川2007))
- 開発情報からのチュートリアルシステム自動生成手法とその評価(推薦論文・FOSE2005)
- ログ解析による操作学習支援システム自動生成
- MANETにおける省資源性を考慮した位置依存情報収集手法(ネットワーク)
- 文書間類似度によるソフトウェアパターン間関連分析と複合関連の導出
- モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般)
- 分岐の相関を利用した効率的なパスプロファイリング
- 多重ループにおける最適ループ展開数算定技法
- 数値演算ループの多次元展開技法
- Java GUIプログラムに対するアクセシビリティチェック(ヒューマンコミュニケーショングループ(HCG)シンポジウム)
- 音階表現によるグラフ形状の理解支援(ヒューマンコミュニケーショングループ(HCG)シンポジウム)
- 大学構内モバイル環境実現における履歴収集機能拡張
- 4X-3 大学構内におけるモバイル環境実現の経験とその評価(学校・教室システム,一般講演,コンピュータと人間社会)
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- JavaFX Scriptで記述されたRIAのアクセシビリティ向上支援
- シーケンス図からの時間性能モデル検査用オブザーバ生成手法(テスト・検証(一般セッション))
- B-052 ソフトウェアパターン文書の解析および体系化(B.ソフトウェア)
- ユースケース間の関係を考慮した網羅的な受け入れテストの支援
- 並列コピーの導入による生存区間分割手法の性能向上
- Javaにおける例外処理の実行時情報を利用した最適化
- コンパイル速度の向上を目的とした非反復型レジスタ割付け手法
- 頻出メソッド管理テーブルを用いたinvokeinterface命令の実行高速化手法
- ページ・機能のモジュール性を高めるWebアプリケーションフレームワークの提案
- センシングプログラムの退避行動を考慮した柔軟なセンサーネットワーク構築(センサネット)
- センシングプログラムの退避行動を考慮した柔軟なセンサーネットワーク構築(センサネット)
- モバイルエージェントによるバッテリ切れ避難システム : EASTER(ネットワーク/モバイル/ユビキタス, ソフトウェアエージェントとその応用論文)
- 多重ループにおける最適ループ展開数算定技法
- REST形式Webサービスのテスト実行に基づく高精度な検索
- 携帯端末用Webページから通常端末用ページを構成する手法 : Webページのモデル化とその評価
- オブジェクト指向'95シンポジウム(OO '95)報告
- 「ソフトウェアアーキテクチャはどう役にたつのか」
- ウィンターワークショップ・イン・沖縄'95開催報告
- フェロモンモデル : 交通渋滞予測への適用(モデル/理論, ソフトウェアエージェントとその応用論文)
- 利用ログに対するウィンドウ遷移の解析による操作学習システム生成
- ユーザの操作を基にしたユーザビリティ自動評価手法
- B-013 音階を用いたグラフ形状の表現システム(B分野:ソフトウェア)
- B-002 Javaソースコードに対するアクセシビリティチェック(B分野:ソフトウェア)
- GUIウィジェット変更に伴うソースコード変更支援
- B-023 ソフトウェアの操作学習支援をする操作マップの自動生成手法(B.ソフトウェア)
- モデル/ビュー分離アーキテクチャBeaMの機構とその評価
- 4C-1 アプリケーション部品についてのMVCパターンの適用
- 特集「アジア・太平洋のソフトウェア技術」の編集にあたって (アジア・太平洋のソフトウェア技術)
- 2.応用プログラム (重点領域研究 : 超並列原理に基づく情報処理基本体系)
- コンポーネント指向Webアプリケーションフレームワークにおけるモジュール性の向上のための一手法
- Model2アーキテクチャのコンポーネント間関係に基づいたWebアプリケーション開発支援
- 標準的使用法の提示によるオブジェクト指向フレームワークの対話的理解支援
- アスペクト指向の導入によるフレームワークの理解容易性の向上
- B-17 オブジェクト指向フレームワークの標準的使用法に基づく対話的理解支援(オブジェクト指向とパターン,B.ソフトウェア)
- フレームワーク製作者の意図を考慮した再構成手法
- 制約記述の導入によるフレームワークのカスタマイズ作法の提示
- 標準的実装からの逸脱度によるフレームワークの設計評価
- スライシングを用いたフレームワークの再構成支援技法
- 5ZC-5 ユーザの実装逸脱度に基づくフレームワークの設計評価メトリクス
- フレームワーク・ナビゲータ : フレームワークを用いたアプリケーション実装の支援
- 仕様記述言語ZZと実行時仕様
- ドメインモデルの形式的記述手法ならびに要求仕様獲得への活用
- プログラム変更に対する正当性検証技法と分割技法の適用
- 論理型仕様の理解支援のための一手法
- RB-006 柔軟かつ複数プログラミング言語対応のテストカバレッジ測定フレームワーク(ソフトウェア,査読付き論文)
- オブジェクト指向フレームワーク上のコンポーネントに対する精度の高いテスト網羅率計測方式の提案
- オブジェクト指向フレームワーク上のコンポーネントに対する精度の高いテスト網羅率計測方式の提案
- 差分概念辞書を用いた過度の仕様抽象度の修正
- プログラムの信頼性向上を目的とした補助スレッドの効率的利用(ジョブスケジューリング, 「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2005))
- プログラムの信頼性向上を目的とした補助スレッドの効率的利用(ジョブスケジューリング, 「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2005))
- プログラムの信頼性向上を目的とした補助スレッドの効率的利用
- レジスタ生存グラフを用いたレジスタ割付けへのプロセッサ並列度の考慮
- B-001 補助スレッドによるソフトウェアの信頼性向上(B.ソフトウェア)
- 領域分割レジスタ生存グラフを用いたレジスタ割付けへの動的計画法の適用
- C-13 レジスタの有効利用を考慮した部分冗長性除去(計算機アーキテクチャと最適化,C.アーキテクチャ・ハードウェア)
- レジスタ生存グラフを用いたレジスタ割付け及びコードスケジューリング技法
- 実行時命令再構成機構を用いた投機的例外復旧手法(21世紀のコンピュータセキュリティ技術)
- ループパーティショニングを用いたショートベクトル化技法
- 制御依存の緩和を考慮した並列性抽出手法
- エージェントフレームワークを用いた車載端末向け情報提供システムの構築と評価(ユビキタスコンピューティングと情報家電)(ユビキタス環境のモバイル通信システムとITS)
- JavaFX ScriptのRIAに対するアクセシビリティライブラリ自動適用手法
- REST形式 Web サービスのテスト実行に基づく高精度な検索
- B-011 既開発部分の解析によるレイアウト調整済みGUIの生成(B分野:ソフトウェア,一般論文)
- 仕様記述言語向きの変換系記述言語TDLの適用と効果
- 仕様記述言語向きの変換系記述言語TDL