UPPAALによるモデル検査適用ガイドラインの作成(解析・検証(一般セッション))
スポンサーリンク
概要
- 論文の詳細を見る
モデル検査によりソフトウェア設計の品質を向上させることが注目されている.一方,モデル検査を開発に適用するノウハウはまだ不足している.本論文ではモデル検査をソフトウェア開発に適用させるためのガイドラインについて報告をする.このガイドラインではモデル検査を実施する目的と効果,モデル検査が適用できる箇所,モデルや検証式を作成する手順,モデルや検証式の記述テクニックの4点について説明を行っている.
- 2008-03-17
著者
-
長谷川 哲夫
株式会社 東芝 ソフトウェア技術センター
-
長谷川 哲夫
(株)東芝研究開発センター
-
長谷川 哲夫
株式会社東芝
-
青木 翼
株式会社東芝
-
宮本 博暢
株式会社東芝
-
渡邊 竜明
株式会社東芝
-
長谷川 哲夫
(株)東芝
関連論文
- Dynagent : 割込みHTNプランニングエージェント
- サービス提供のためのネットワークロボット連携技術
- モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般)
- Lagrange緩和法を用いた最適化スケジューリングにおけるheuristicsのアプローチ(スケジューリング(3))
- Lagrange緩和法によるスケジューリングの実用化 : (2)実行可能解の構成(生産計画(3))
- Lagrange緩和法によるスケジユーリングの実用化 : (1)問題の抽象化と解の具体化(生産計画(3))
- ホロニック手法による組立システムのプランニング
- UPPAALによるモデル検査適用ガイドラインの作成(解析・検証(一般セッション))
- シーケンス図からの時間性能モデル検査用オブザーバ生成手法(テスト・検証(一般セッション))
- ロボットをユビキタスの世界へ誘うエージェント (特集 ホームロボット技術--ロボット技術で支える安心・安全な暮らし)