抽象化に基づいた UML設計の検証支援ツールの開発

2013年度ソフトウェア工学分野の先導的研究支援事業
抽象化に基づいた
UML設計の検証支援ツールの開発
公立大学法人岡山県立大学
情報工学部情報システム工学科
横川智教
Circuit Design Engineering Lab. - Okayama Prefectural University
背景 - 組込みソフトウェア開発の課題
組込みソフトウェアの開発プロセス
要求分析
設計
実装
テスト
手戻り
下流工程での不具合の検出
上流工程への手戻りの発生
手戻りによる開発コスト増大
設計検証の必要性の高まり
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
2
Circuit Design Engineering Lab. - Okayama Prefectural University
背景 - 組込みソフトウェアの設計検証
設計ドキュメント
要求仕様
どの状態にも
いつか必ず到達する
危険な状態には
決して到達しない
ある変数が定められた
値に必ず到達する
UML(状態マシン図)
・・・
作成された設計ドキュメントが
要求仕様を満たしているか？
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
3
Circuit Design Engineering Lab. - Okayama Prefectural University
背景 - 設計検証の困難さ
従来の枠組み（テスト・レビュー）で組込みソフトウェアの
設計検証を行うのは非常に困難である
理由
1. 組込みソフトウェアの不具合が社会に及ぼす影響が
甚大であり，信頼性への要求のハードルが非常に高
い
2. ソフトウェアの大規模・複雑化により，システムの
取り得る状態数が人手でテストを行う限界を遙かに
越えている
網羅的かつ自動検証が可能なモデル検査技術の利用
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
4
Circuit Design Engineering Lab. - Okayama Prefectural University
モデル検査
モデル検査とは
状態遷移系でモデル化されたシステムの全数探索により
求める特性を満たすか否かを自動検証する技術
モデル検査の適用
1. モデル化言語により検査対象システム（仕様書・設計
書・回路図 etc.）を記述
2. 論理式として検査項目（要求仕様・試験仕様・基本性
質・客先要望 etc.）を記述
3. モデル検査ツールによる自動探索の実施
4. モデルが検査項目を満たすという証明か，満たさない場
合は反例を出力
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
5
Circuit Design Engineering Lab. - Okayama Prefectural University
研究課題
モデル検査を設計検証に導入する上での問題点
問題１．モデル作成の困難さ
対象システムを検証ツール固有のモデル化言語で記述
モデル作成には専門的な知識やノウハウが必要
問題２．状態爆発の危険性
モデル化された対象システムの状態空間を網羅的探索
モデル規模によっては検証に莫大な時間を要する
モデル作成を支援するためのツールを開発し問題を解決
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
6
Circuit Design Engineering Lab. - Okayama Prefectural University
検証支援ツール
前提
1. 対象とする設計記法として，組込みソフトウェア開発に
広く利用されている形式仕様記法UMLを想定する
2. モデル検査ツールとして，モデル記述言語の表現力およ
び検証速度に優れたNuSMVを利用する
ツールの機能
1. SMV言語への自動変換を目的としたUML図の抽象化
2. モデルサイズ削減を目的としたUML図の抽出・分割およ
び抽象化
3. UML図からSMV言語への自動変換
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
7
Circuit Design Engineering Lab. - Okayama Prefectural University
検証支援ツールの概要
要求仕様
(*.ctl)
UML図
(*.asta)
入
力
イ
ン
タ
フ
ェ
ー
ス
仕様
テンプレート
要求仕様
記述制約
UML図
UMLモデリングツール
astah*
抽
象
化
・
変
換
モ
ジ
ュ
ー
ル
検証モデル
(*.smv)
検証結果
(*.out)
モデル検査ツール
NuSMV
出
力
イ
ン
タ
フ
ェ
ー
ス
検証結果
(整形済)
(*.result)
違反箇所
情報
(*.ce)
検証支援ツール
外部ツール
 UML図の記述にはastah*を，検証にはNuSMVを用いる
 UML図が満たすべき記述制約と，要求仕様を記述するため
の仕様テンプレートが定められている
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
8
Circuit Design Engineering Lab. - Okayama Prefectural University
SMV言語による検証モデル生成の流れ
MODULE main
VAR
XXX : {aaa, bbb, ccc};
YYY : {ddd, eee, fff};
fg1 : boolean;
モデル生成
状態マシン図
モデル
init(YYY) := ddd;
next(YYY) := case
fg = FALSE : fff
TRUE : YYY;
esac;
シーケンス図
UML図ファイル(*.asta)
safe(xxx = 1)
live(message_1)
reachable(S)
要求仕様ファイル(*.ctl)
2014/05/22
ASSIGN
init(XXX) := aaa;
next(XXX) := case
fg = TRUE : bbb;
TRUE : XXX;
esac;
CTL式
生成
init(fg) := FALSE;
next(fg) := case
fg = FALSE : {TRUE, FALSE};
TRUE : fg;
esac;
SPEC AG !(XXX = ccc)
SPEC EF(ZZZ = iii)
SPEC AF(YYY = fff)
CTL式
検証モデルファイル(*.smv)
第2回産学連携のためのソフトウェアシンポジウム
9
Circuit Design Engineering Lab. - Okayama Prefectural University
事例適用による評価
 経緯
– 某ソフトウェア開発企業に事例提供を打診
– 開発に用いた状態遷移表からUML図(状態マシン図)
を作成
– 対象システムは店舗従業員向けの「商品供給指示シ
ステム」
› 売場の端末と商品管理室のモニターの間で，商品供給の
ための通信を行う
 検査項目
– 検査１：仕様テンプレートを用いた基本特性の検査
– 検査２：事例提供元より要望のあった特性の検査
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
10
Circuit Design Engineering Lab. - Okayama Prefectural University
検査対象となるUML図
端末が２台の場合の状態遷移表とモニターの表示方法を
元に状態マシン図を作成したものを提供いただいた
端末A
モニター
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
端末B
UML図ファイル
R_CDS.asta
11
Circuit Design Engineering Lab. - Okayama Prefectural University
検査１
仕様テンプレートを用いて以下の検査を行った
•
•
•
•
端末状態の到達可能性
通信モード(使用回線数)の到達可能性
通信モードの安全性
商品管理室のモニターの到達可能性
検査項目
状態の到達可能性
テンプレート
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)
要求仕様
ファイル
BASIC.ctl
safe(MD_B, 3)
safe(MD_B, -1)
モニターの到達可能性
2014/05/22
reachable(s)
reachable(Ctl_Monitor = surplus)
reachable(Ctl_Monitor = sufficient)
reachable(Ctl_Monitor = optimal)
reachable(Ctl_Monitor = few)
reachable(Ctl_Monitor = short)
第2回産学連携のためのソフトウェアシンポジウム
12
Circuit Design Engineering Lab. - Okayama Prefectural University
本ツールの適用結果(検査１)
R_CDS.asta
BASIC.ctl
本ツールを用いて
SMVファイルを生成
R_CDS_BASIC.smv
モデル検査器
NuSMVで検査
R_CDS_BASIC.out
検査結果の
整形
(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 = optimal is true
(018) EF Ctl_Monitor = few is true
(019) EF Ctl_Monitor = short is true
R_CDS_BASIC.result
R_CDS_BASIC.result
全ての結果がTRUE
2014/05/22
誤りは存在しない
第2回産学連携のためのソフトウェアシンポジウム
13
Circuit Design Engineering Lab. - Okayama Prefectural University
検査２
事例提供元より要望があり，以下の検査を行った
1.
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)
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
要求仕様ファイル
R_CDS_REQ.ctl
14
Circuit Design Engineering Lab. - Okayama Prefectural University
本ツールの適用結果(検査２)
R_CDS.asta
R_CDS_REQ.ctl
R_CDS_REQ.smv
同様にファイル生成し検証した結果，
誤りを検出し反例(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(一部)
R_CDS_REQ.out
R_CDS_REQ.result
R_CDS_REQ.ce
(003) !(EF (Terminal_A = com & MD_A = 0)) is false
-> State: 1.1 <Terminal_A = initial
MD_A = 0
Power = start
Event_A = emp
…
R_CDS_REQ.ce(一部)
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
15
Circuit Design Engineering Lab. - Okayama Prefectural University
本ツールの適用結果(検査２)
特性3Aに対する反例の解析
1
2
3
4
5
Event_A
emp
emp
report
response
emp
MD_A
0
0
0
0
0
Terminal_A
initial
initial
wait
send
com
端末が通信中(Terminal_A=com)であるにもかかわらず，
通信モードが通話無し(MD_A=0)となる状態に到達している
状態遷移表のアクションの１つが
UML図に正しく転記されていなかった
• UML図による設計の誤りを正しく検出できた
• 反例を元に誤り箇所を特定することができた
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
16
Circuit Design Engineering Lab. - Okayama Prefectural University
研究成果の産業界への寄与
本ツールが果たす役割
• 組込みソフトウェア開発における設計検証のサポート
• UML設計記述からモデル検査ツールの入力モデルへの
変換の大部分を自動化
• ツールによって得られた結果を整形して表示
• 抽象化により高速化な検証を実現
組込みソフトウェア開発の設計検証に対する
モデル検査技術の導入促進
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
17
Circuit Design Engineering Lab. - Okayama Prefectural University
研究成果の産業界への寄与
本ツールを導入するメリット
• 開発コストの削減
• 自動検証の実現により人的・時間的なコストを削減
• ソフトウェア信頼性の担保
• 証明されたアルゴリズムを利用することで，結果に
ついては完全に保証可能
導入にあたって必要なこと
• 開発環境
• UMLを用いた設計
• astah* communityの利用
2014/05/22
第2回産学連携のためのソフトウェアシンポジウム
18
Circuit Design Engineering Lab. - Okayama Prefectural University

Download Report