| Item type |
FIT(1) |
| 公開日 |
2010-08-20 |
| タイトル |
|
|
タイトル |
B-017 時間制約を持つ仕様に対するUML/SysMLモデルの動的検査手法(B分野:ソフトウェア,一般論文) |
| タイトル |
|
|
言語 |
en |
|
タイトル |
B-017 A Dynamic Verification Method of UML/SysML Models with Timed Constraints |
| 言語 |
|
|
言語 |
jpn |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
日本アイ・ビー・エム株式会社東京基礎研究所 |
| 著者所属 |
|
|
|
日本アイ・ビー・エム株式会社東京基礎研究所 |
| 著者所属 |
|
|
|
日本アイ・ビー・エム株式会社東京基礎研究所 |
| 著者所属 |
|
|
|
日本アイ・ビー・エム株式会社東京基礎研究所 |
| 著者所属(英) |
|
|
|
en |
|
|
IBM Research-Tokyo |
| 著者所属(英) |
|
|
|
en |
|
|
IBM Research-Tokyo |
| 著者所属(英) |
|
|
|
en |
|
|
IBM Research-Tokyo |
| 著者所属(英) |
|
|
|
en |
|
|
IBM Research-Tokyo |
| 著者名 |
小野, 康一
河原, 亮
中村, 宏明
石川, 浩
|
| 著者名(英) |
Ono, Kouichi
KAWAHARA, Ryo
NAKAMURA, Hiroaki
ISHIKAWA, Hiroshi
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
UML/SysMLによる実行可能なシステム・モデルの振舞が,時間/機能制約による仕様に対して整合するかどうかを動的に検査する技術を提案する.制御系の離散的振舞と機械系/電気系の連続的振舞の連携を必要とすることが多い組込みシステム/リアルタイムシステムのモデルでは,制御系のモデルを形式手法などで静的に検証するだけでは不十分であり,動的検査が必要となる.また,開発早期において分析レベル・モデルを用いて性能などの非機能要件の充足性を判断するのにこの検査技術は特に有効である.仕様は,時間/機能制約を付与したシーケンス図の集合で定義する.動的検査は,システム・モデルの実行トレースとして取得するモデル・イベントの列を,シーケンス図に表現されるイベント・パターンおよび制約条件の集合と照合する問題として実現することができる.シーケンス図の集合をイベント・パターンの相違に対応した二分木の集合にあらかじめ変換しておくことで,モデル実行の迅速な検査や,長時間に亘る大量の実行トレースからの仕様との不整合箇所の発見が可能になる. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA1242354X |
| 書誌情報 |
情報科学技術フォーラム講演論文集
巻 9,
号 1,
p. 299-306,
発行日 2010-08-20
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
KJ00006916951.pdf (849.1 kB)
