2013
年年度度ソフトウェア⼯工学分野の先導的研究⽀支援事業
抽象化に基づいた
UML
設計の検証⽀支援ツールの開発
横川 智教
公⽴立立⼤大学法⼈人岡⼭山県⽴立立⼤大学
情報⼯工学部 情報システム⼯工学科
背景 -‐ 組込みソフトウェア開発の課題
要求分析
設計
実装
テスト
⼿手戻り
組込みソフトウェアの開発プロセス
下流流⼯工程での
不不具合
の検出
上流流⼯工程への
⼿手戻り
の発⽣生
⼿手戻りによる
開発コスト増⼤大
設計検証
の必要性の⾼高まり
背景 -‐ 組込みソフトウェアの設計検証
設計ドキュメント
どの状態にも
いつか必ず到達する
危険な状態には
決して到達しない
ある変数が定められた
値に必ず到達する
UML(
状態マシン図
)
・・・
作成された設計ドキュメントが
要求仕様を満たしているか？
要求仕様
背景 -‐ 設計検証の困難さ
理理由
1.
組込みソフトウェアの不不具合が社会に及ぼす影響が
甚⼤大であり，
信頼性への要求のハードルが⾮非常に⾼高
い
2.
ソフトウェアの⼤大規模・複雑化により，システムの
取り得る状態数が
⼈人⼿手でテストを⾏行行う限界を遙かに
越えている
従来の枠組み（テスト・レビュー）で組込みソフトウェアの
設計検証を⾏行行うのは⾮非常に困難である
網羅羅的かつ⾃自動検証が可能な
モデル検査技術
の利利⽤用
モデル検査
モデル検査とは
状態遷移系でモデル化されたシステムの
全数探索索
により
求める特性を満たすか否かを
⾃自動検証
する技術
モデル検査の適⽤用
1.
モデル化⾔言語により検査対象システム（仕様書・設計
書・回路路図 etc.）を記述
2.
論論理理式として検査項⽬目（要求仕様・試験仕様・基本性
質・客先要望 etc.）を記述
3.
モデル検査ツールによる⾃自動探索索の実施
4.
モデルが検査項⽬目を満たすという
証明
か，満たさない場
合は
反例例
を出⼒力力
研究課題
モデル検査を設計検証に導⼊入する上での
問題点
問題１．モデル作成の困難さ
対象システムを検証ツール固有のモデル化⾔言語で記述
モデル作成には
専⾨門的な知識識
や
ノウハウ
が必要
問題２．状態爆発の危険性
モデル化された対象システムの状態空間を網羅羅的探索索
モデル規模によっては検証に
莫⼤大な時間
を要する
検証⽀支援ツール
1.
対象とする設計記法として，組込みソフトウェア開発に
広く利利⽤用されている形式仕様記法
UML
を想定する
2.
モデル検査ツールとして，モデル記述⾔言語の表現⼒力力およ
び検証速度度に優れた
NuSMV
を利利⽤用する
ツールの機能
1. SMV
⾔言語への⾃自動変換を⽬目的としたUML図の抽象化
2.
モデルサイズ削減を⽬目的としたUML図の抽出・分割およ
び抽象化
3. UML
図からSMV⾔言語への⾃自動変換
前提
検証⽀支援ツールの概要
⼊入
⼒力力
イ
ン
タ
フ
ー
ス
UML
モデリングツール
astah*
仕様
テンプレート
要求仕様
UML図
(*.asta)
要求仕様
(*.ctl)
抽
象
化
・
変
換
モ
ジ
ー
ル
検証モデル
(*.smv)
検証結果
(*.out)
検証結果
(整形済)
(*.result)
違反箇所
情報
(*.ce)
記述制約
UML図
モデル検査ツール
NuSMV
出
⼒力力
イ
ン
タ
フ
ー
ス
検証⽀支援ツール
外部ツール
l
UML
図の記述には
astah*
を，検証には
NuSMV
を⽤用いる
SMV
⾔言語による検証モデル⽣生成の流流れ
SPEC AG !(XXX = ccc) SPEC EF(ZZZ = iii) SPEC AF(YYY = fff) MODULE main VAR XXX : {aaa, bbb, ccc}; YYY : {ddd, eee, fff}; fg1 : boolean; ASSIGN init(XXX) := aaa; next(XXX) := case fg = TRUE : bbb; TRUE : XXX; esac; init(YYY) := ddd; next(YYY) := case fg = FALSE : fff TRUE : YYY; esac; init(fg) := FALSE; next(fg) := case
fg = FALSE : {TRUE, FALSE}; TRUE : fg; esac;
状態マシン図
シーケンス図
UML
図ファイル(*.asta)
モデル
CTL
式
モデル⽣生成
CTL
式
⽣生成
safe(xxx = 1)
live(message_1)
reachable(S)
事例例適⽤用による評価
l
経緯
–
某ソフトウェア開発企業に事例例提供を打診
–
開発に⽤用いた状態遷移表から
UML
図(状態マシン図)を作成
–
対象システムは店舗従業員向けの
「商品供給指⽰示システム」
›
売場の端末と商品管理理室のモニターの間で，
商品供給のための通信を⾏行行う
l
検査項⽬目
–
検査１：仕様テンプレートを⽤用いた基本特性の検査
–
検査２：事例例提供元より要望のあった特性の検査
検査対象となるUML図
2
台の売場端末とモニター表⽰示の動作の状態マシン図
(
状態遷移表を元に作成)
UML
図ファイル
R_CDS.asta
端末A
端末B
モニター
検査１
仕様テンプレートを⽤用いて４つの基本特性を記述
検査項⽬目
テンプレート
ツールへの⼊入⼒力力
状態の到達可能性
reachable(s)
reachable(Terminal_A = send)
reachable(Terminal_A = receive)
reachable(Terminal_A = com)
reachable(Terminal_B = send)
reachable(Terminal_B = receive)
reachable(Terminal_B = com)
通信モードの到達可能性 reachable(x,a)
reachable(MD_A, 1)
reachable(MD_A, 2)
reachable(MD_B, 1)
reachable(MD_B, 2)
通信モードの安全性
safe(x,a)
safe(MD_A, 3)
safe(MD_A, -‐1)
safe(MD_B, 3)
safe(MD_B, -‐1)
モニターの到達可能性
reachable(s)
reachable(Ctl_Monitor = surplus)
reachable(Ctl_Monitor = sufficient)
reachable(Ctl_Monitor = opdmal)
要求仕様
ファイル
BASIC.ctl
本ツールの適⽤用結果(検査１)
本ツールを⽤用いて
SMV
ファイルを⽣生成
R_CDS.asta
BASIC.ctl
R_CDS_BASIC.smv
モデル検査器
NuSMV
で検査
R_CDS_BASIC.out
R_CDS_BASIC.result
検査結果の
整形
(001) EF Terminal_A = send is true (002) EF Terminal_A = receive is true (003) EF Terminal_A = com is true (004) EF Terminal_B = send is true (005) EF Terminal_B = receive is true (006) EF Terminal_B = com is true (007) EF MD_A = 1 is true
(008) EF MD_A = 2 is true (009) EF MD_B = 1 is true (010) EF MD_B = 2 is true (011) AG !(MD_A = 3) is true (012) AG !(MD_A = -‐1) is true (013) AG !(MD_B = 3) is true (014) AG !(MD_B = -‐1) is true
(015) EF Ctl_Monitor = surplus is true (016) EF Ctl_Monitor = sufficient is true (017) EF Ctl_Monitor = opdmal is true (018) EF Ctl_Monitor = few is true (019) EF Ctl_Monitor = short is true
検査２
事例例提供元より要望のあった特性を直接検査式として記述
1.
端末が待機状態であり，かつ通信モードが通話無しでない
状態への到達可能性
2.
端末が着信中状態であり，かつ通信モードが2回線通話である
状態への到達可能性
3.
端末が通話中であり，かつ通信モードが通話無しである
状態への到達可能性
1A: SPEC !EF(Terminal_A = wait & !(MD_A = 0))
2A: SPEC !EF(Terminal_A = receive & MD_A = 2)
2A: SPEC !EF(Terminal_A = com & MD_A = 0)
1B: SPEC !EF(Terminal_B = wait & !(MD_B = 0))
2B: SPEC !EF(Terminal_B = receive & MD_B = 2)
3B: SPEC !EF(Terminal_B = com & MD_B = 0)
要求仕様ファイル
R_CDS_REQ.ctl
本ツールの適⽤用結果(検査２)
R_CDS.asta
R_CDS_REQ.ctl
R_CDS_REQ.smv
R_CDS_REQ.out
R_CDS_REQ.result
R_CDS_REQ.ce
(001) !(EF (Terminal_A = wait & !(MD_A = 0))) is true
(002) !(EF (Terminal_A = receive & MD_A = 2)) is true
(003) !(EF (Terminal_A = com & MD_A = 0)) is
false
…
R_CDS_REQ.result(
⼀一部)
(003) !(EF (Terminal_A = com & MD_A = 0)) is false
-‐> State: 1.1 <-‐
Terminal_A = inidal
MD_A = 0
Power = start
Event_A = emp
…
結果が
FALSE
誤りを検出し，
反例例
を出⼒力力
本ツールの適⽤用結果(検査２)
特性3Aに対する反例例の解析
1
2
3
4
5
Event_A
emp
emp
report
response
emp
MD_A
0
0
0
0
0
Terminal_A
inidal
inidal
wait
send
com
端末が通信中(Terminal_A=com)であるにもかかわらず
，
通信モードが通話無し(MD_A=0)となる状態に到達している
•
UML
図による設計の誤りを正しく検出できた
•
反例例を元に誤り箇所を特定することができた
原因：状態遷移表のアクションの１つが
UML図に正しく転記されていなかった
まとめ
ツールデモ
本ツールのデモを岡⼭山県⽴立立⼤大学の
ブース(
U-‐06
)
内にて実施しています．
お気軽にお越しください．
オムロン ソフトウェア ウルトラ エックス バルテス・モバイルテクノロジーテレダイン・ レクロイ・ ジャパン ベリサーブ バルテス ユニダックス アバールデータ RITA エレクトロニクス A-12 A-08 A-07 A-06 A-11 A-10 A-09 A-05 組込みシステム 産業振興機構 A-04 アドバンスド・データ・ コントロールズ A-01 九州 工業大学大阪電気通信大学大学院 GENET／奈良工業 展示会登録所 BEMS/FEMS/ HEMS/MEMS ゾーン IoT ゾーンU-01 U-01 U-01
イーソル GENUSION 星和電機 近藤電子工業 アズマ 窓飛 ビットラン B-14 B-10 B-09 B-08 B-13 B-12 B-11 B-07 ノリタケ伊勢電子 イー・フォース 暁電機 製作所 ナムコール製作所金沢工業大学・北陸先端科学技術 大学院大学 iTest アイエーアール・ システムズ プライム ゲート C-26 グレープ システム C-18 C-22 C-21 C-20 C-25 C-24 C-23 C-13 オンテック とめ 研究所日本キャステム TOPPERS プロジェクト NSCore C-15 C-14 C-17 C-16 C-13 三菱電機 インフォメーション システムズ C-06 アルゴシステム スパークス システムズジャパンHMSインダストリアルネットワークス セカンド セレクション レジェンド C-03 C-02 C-05 C-04 C-01 アイティアクセス B-06 中央電子 ファームウェアシステム共和電子製作所 シグマ電子工業 アトラシアン B-03 B-02 B-05 B-04 B-01 日本システムウエア 東京コスモス電機 長野 日本無線 東海 ソフトBee 日本マイクロ システムズ 山電器 日新 システムズ D-10 D-06 D-05 D-04 YAMABISHI スマート ジャパン アライアンス 富士経済 エブリ D-16 D-17 D-15 D-14 dSPACED-13Japan イメディオ パビリオン 関西積乱雲 プロジェクト D-12 D-11 D-09 D-08 D-07 D-03 本田技研工業 D-02 日本アルテラ D-01 キヤノン ソフトウェア フリースケール・セミコンダクタ・ ジャパン エルイーテック 日立 ソリューションズ コアスタッフ ベリフィケーション テクノロジー B-22 B-17 B-21 B-20 B-19 B-18 アルファ プロジェクト ARKUS 日本パルス モーター イノテック C-12 C-11 C-10 アドバネット
Chips &C-09Media C-08 C-07 コア B-16 たけびし EMS-JPグループ Spansion ハギワラ ソリューションズ 情報処理推進機構（IPA） インターナショナルディジ 総合設備日比谷 ルーム2+3 基調講演 ルーム1 IPAセミナー ルーム7 スマートエネルギーセミナー／ 出展社セミナー／ Digi M2M CONFERENCE 2014 Osaka ルーム8 IoTトラック／ 出展社セミナー ルーム9 テクニカルセッション／ 出展社セミナー C-28 C-27 B-23 B-15 A-13 A-03 A-02 岡山県立大学 情報工学部 名古屋大学大学院 情報科学研究科付属 U-04 U-05 U-06
オムロン ソフトウェア ウルトラ エックス バルテス・モバイル テクノロジー テレダイン・ レクロイ・ ジャパン ベリサーブ バルテス ユニダックス アバールデータ RITA エレクトロニクス A-12 A-08 A-07 A-06 A-11 A-10 A-09 A-05 組込みシステム 産業振興機構 A-04 アドバンスド・データ・ コントロールズ A-01 九州 工業大学大阪電気通信大学大学院 GENET／ 奈良工業 高等専門学校 ユニバーシティパビリオン 展示会登録所 BEMS/FEMS/ HEMS/MEMS ゾーン IoT ゾーン
U-01 U-01 U-01
イーソル GENUSION 星和電機 近藤電子工業 アズマ 窓飛 ビットラン B-14 B-10 B-09 B-08 B-13 B-12 B-11 B-07 ノリタケ伊勢電子 イー・フォース 暁電機 製作所 ナムコール 製作所 金沢工業大学・ 北陸先端科学技術 大学院大学 iTest アイエーアール・ システムズ プライム ゲート C-26 グレープ システム C-18 C-22 C-21 C-20 C-25 C-24 C-23 C-13 オンテック とめ 研究所 日本キャステム TOPPERS プロジェクト NSCore C-15 C-14 C-17 C-16 C-13 三菱電機 インフォメーション システムズ C-06 アルゴシステム スパークス システムズ ジャパン HMS インダストリアル ネットワークス セカンド セレクション レジェンド C-03 C-02 C-05 C-04 C-01 アイティアクセス B-06 中央電子 ファームウェア システム共和電子製作所 シグマ電子工業 アトラシアン B-03 B-02 B-05 B-04 B-01 日本システムウエア 東京コスモス電機 長野 日本無線 東海 ソフト Bee 日本マイクロ システムズ 山電器 日新 システムズ D-10 D-06 D-05 D-04 YAMABISHI スマート ジャパン アライアンス 富士経済 エブリ D-16 D-17 D-15 D-14 dSPACE Japan D-13 イメディオ パビリオン 関西積乱雲 プロジェクト D-12 D-11 D-09 D-08 D-07 D-03 本田技研工業 D-02 日本アルテラ D-01 キヤノン ソフトウェア フリースケール・ セミコンダクタ・ ジャパン エルイーテック 日立 ソリューションズ コアスタッフ ベリフィケーション テクノロジー B-22 B-17 B-21 B-20 B-19 B-18 アルファ プロジェクト ARKUS 日本パルス モーター イノテック C-12 C-11 C-10 アドバネット Chips & Media C-09 C-08 C-07 コア B-16 たけびし EMS-JPグループ Spansion ソリューションズハギワラ 情報処理推進機構（IPA） インターナショナルディジ 総合設備日比谷 ルーム2+3 基調講演 ルーム1 IPAセミナー ルーム7 スマートエネルギーセミナー／ 出展社セミナー／ Digi M2M CONFERENCE 2014 Osaka ルーム8 IoTトラック／ 出展社セミナー ルーム9 テクニカルセッション／ 出展社セミナー C-28 C-27 B-23 B-15 A-13 A-03 A-02 立命館大学電子情報工学科 ネットワークLSIシステム研究室 岡山県立大学 情報工学部 情報システム工学科 回路デザイン研究室 名古屋大学大学院 情報科学研究科付属 組込みシステム研究センター ユニバーシティパビリオン
U-04 U-05 U-06
