UPPAALによるモデル検査適用ガイドラインの作成(解析・検証(一般セッション))
スポンサーリンク
概要
- 論文の詳細を見る
モデル検査によりソフトウェア設計の品質を向上させることが注目されている.一方,モデル検査を開発に適用するノウハウはまだ不足している.本論文ではモデル検査をソフトウェア開発に適用させるためのガイドラインについて報告をする.このガイドラインではモデル検査を実施する目的と効果,モデル検査が適用できる箇所,モデルや検証式を作成する手順,モデルや検証式の記述テクニックの4点について説明を行っている.
- 2008-03-17
著者
-
長谷川 哲夫
株式会社 東芝 ソフトウェア技術センター
-
長谷川 哲夫
(株)東芝研究開発センター
-
長谷川 哲夫
株式会社東芝
-
青木 翼
株式会社東芝
-
宮本 博暢
株式会社東芝
-
渡邊 竜明
株式会社東芝
-
長谷川 哲夫
(株)東芝
関連論文
- Dynagent : 割込みHTNプランニングエージェント
- サービス提供のためのネットワークロボット連携技術
- モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般)
- Lagrange緩和法を用いた最適化スケジューリングにおけるheuristicsのアプローチ(スケジューリング(3))
- Lagrange緩和法によるスケジューリングの実用化 : (2)実行可能解の構成(生産計画(3))
- Lagrange緩和法によるスケジユーリングの実用化 : (1)問題の抽象化と解の具体化(生産計画(3))
- ホロニック手法による組立システムのプランニング
- UPPAALによるモデル検査適用ガイドラインの作成(解析・検証(一般セッション))
- シーケンス図からの時間性能モデル検査用オブザーバ生成手法(テスト・検証(一般セッション))
- ロボットをユビキタスの世界へ誘うエージェント (特集 ホームロボット技術--ロボット技術で支える安心・安全な暮らし)
- 携帯電話上で記述・即時動作可能なネットワークスクリプトの開発
- ホロニック生産システムのアーキテクチャ
- セマンティック Web サービスマッチメーカーの公開実験に基づく評価
- ユビキタスアプリケーション向け移動エージェントの相互運用
- XML Webサービスのマッチメーカー (特集1 XML Webサービス--インターネット上でサービスをダイナミックに連携)
- マルチエージェントフレームワークBee-gentを用いた電力系統作業停止計画向け分散スケジューリングシステムの開発
- 移動エージェント相互運用の実現 : 基本アーキテクチャ
- 3W-6 マルチエージェントフレームワークBee-gentのためのビジュアル開発支援ツール
- 3S-10 マルチエージェントフレームワークBee-gentによる環境調和型製品設計支援システムの開発
- 3S-4 移動エージェント相互運用の実現 : ディレクトリサーバ
- 3S-3 移動エージェント相互運用の実現 : インカネーションエージェントによる相互運用の実現
- 3S-2 移動エージェント相互運用の実現 : 基本アーキテクチャ
- 3S-1 移動エージェント相互運用の実現 : 背景と構想
- Bee-gent:移動型仲介エージェントによる既存システムの柔軟な活用を目的としたマルチエージェントフレームワーク
- マルチエージェントフレームワークBee-gentを用いた分散システムにおけるデザインパラダイムの分類と評価
- 既存システムの柔軟な結合を可能にするエージェントフレームワークBe-gentの提案
- モバイルエージェントを用いた分散制約充足問題へのアプローチ : 分散協調型電力系統設備作業停止計画支援システムの開発
- ホロニック生産システムの協調機構
- 4.3 高信頼分散システム構築支援OS : 知的分散^OS (日本におけるオペレーティングシステム研究の動向)
- 知的分散OS : 放送型オブジェクト指向分散OS
- D-9-8 PCリモートアクセスシステム・ユビキタスビューアの開発 : 携帯電話版の開発(D-9.オフィスインフォメーションシステム,一般講演)
- D-9-7 PCリモートアクセスシステム・ユビキタスビューアの開発 : システムアーキテクチャ(D-9.オフィスインフォメーションシステム,一般講演)
- ENC(Enhanced Network Computing)フレームワークの概要