組込みソフトウェア検証へのモデル検査技術の導⼊に関する技術動向

横川 智教
t‐yokoga@cse.oka‐pu.ac.jp

岡⼭県⽴⼤学Circuit Design Engineering Lab. ‐ Okayama Prefectural University

講師紹介
 所属

– 岡⼭県⽴⼤学› 情報⼯学部情報システム⼯学科› 回路デザイン研究室・助教

 最近の研究テーマ– モデル検査による組込みソフトウェアの設計検証– ⾮同期回路のモデル化・性能評価・検証

 連絡先– t‐yokoga@cse.oka‐pu.ac.jp– http://circuit.cse.oka‐pu.ac.jp/2014/09/01

SES2014チュートリアル

2
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

本チュートリアルの概要
 はじめに – モデル検査とは– 形式⼿法とは？

› どんな⼿法がある？
› どんなツールがある？

 組込みソフトウェア開発への導⼊事例– モデル検査の導⼊事例– そのほかの形式⼿法の導⼊事例

 モデル検査によるUML設計検証⽀援ツール– ツールの概要› ツールを利⽤するための準備› ツールの使い⽅について– 適⽤事例
2014/09/01

SES2014チュートリアル

3Circuit Design Engineering Lab. ‐ Okayama Prefectural University

本チュートリアルの概要
 はじめに – モデル検査とは– 形式⼿法とは？

› どんな⼿法がある？
› どんなツールがある？

 組込みソフトウェア開発への導⼊事例– モデル検査の導⼊事例– そのほかの形式⼿法の導⼊事例

 モデル検査によるUML設計検証⽀援ツール– ツールの概要› ツールを利⽤するための準備› ツールの使い⽅について– 適⽤事例
2014/09/01

SES2014チュートリアル

4Circuit Design Engineering Lab. ‐ Okayama Prefectural University

モデル検査形式⼿法(formal method)の⼀種– システムの⾃動検証技術– システムを状態遷移グラフでモデル化し，モデルの網羅的探索によって求める特性を満たすか否かを⾃動的に判定に到達することはできるか？

からは必ずに到達するか？

状態遷移グラフ2014/09/01

SES2014チュートリアル

5
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

形式⼿法
 形式⼿法とは– システム開発に数学・論理学を導⼊するための技術› ⼿続きの⾃動化による品質向上・コスト削減

 形式⼿法の利⽤– 仕様記述› 集合論に基づいてデータ構造を記述› 述語論理を⽤いてシステムの要求を表現– 開発› プロセス代数論により要求と設計の等価性判定– 検証› 公理によるプログラム証明› グラフ探索アルゴリズムによる特性検証

2014/09/01

SES2014チュートリアル

6
Circuit Design Engineering Lab. ‐ Okayama Prefectural University主な形式⼿法
形式仕様記述(formal specification)– システムの仕様を集合論や論理式を⽤いて数学的に表現するための記法– 抽象的かつ厳密な記述

形式的証明(formal reasoning)– 形式的な⼿続きに基づいてシステムの正しさを証明するための技術– 定理証明とモデル検査に分類される
2014/09/01SES2014チュートリアル

7
Circuit Design Engineering Lab. ‐ Okayama Prefectural University形式的証明 定理証明(theorem proving)– 公理と推論規則に基づいてシステムの性質を証明– 完全に⾃動化することは困難とされる– 証明の⾃動⽣成を⽀援するツールは存在 モデル検査(model checking)– 状態遷移グラフでモデル化されたシステムの網羅的探索に基づいて求める性質を満たすか検証– 完全に⾃動化された⼿続き› 有限状態システムのみが対象– 状態爆発への対処が課題
2014/09/01

SES2014チュートリアル

8
Circuit Design Engineering Lab. ‐ Okayama Prefectural University主な形式仕様記法
Z– 集合論，述語論理，λ計算の記法に基づいてプログラムの仕様と振る舞いを記述する

 B, Event‐B– 段階的詳細化により仕様記述からプログラム⽣成を⾏う⼿法(Bメソッド)において⽤いられる

 CSP– プロセス代数論に基づいて，並⾏動作するプロセス群の相互作⽤を記述する

 SCADE– 同期型プログラミング⾔語であり，時間に同期して動作するリアルタイムシステムの記述が可能

2014/09/01

SES2014チュートリアル

9Circuit Design Engineering Lab. ‐ Okayama Prefectural University主な定理証明⽀援ツール
PVS– 集合論に基づく仕様記述⾔語と検証ツールによって構成– 対話的な定理証明が可能

Coq– 定理証明⽀援⾔語– Coq⾔語で記述したプログラムに対する証明が可能

2014/09/01

SES2014チュートリアル

10
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

主なモデル検査ツール(1)SPIN– 分散システムを対象としたモデル検査ツール– 時相論理LTLで検証する特性を記述– システムと特性をオートマトンでモデル化

FDR– CSPモデルを対象としたモデル検査ツール– プロセスの模倣性検証が可能

VDM‐Tools– 形式仕様記法VDM‐SL,VDM++で記述された仕様の検証や実⾏が可能
2014/09/01

SES2014チュートリアル

11
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

主なモデル検査ツール(2)SMV– 記号モデル検査アルゴリズムに基づいた⾼速な検証が可能– 専⽤⾔語(SMV⾔語)で検査対象システムを記述– 時相論理CTLで検証する特性を記述

UPPAAL– リアルタイムシステムを対象としたモデル検査ツール– 時間オートマトンで検査対象システムを記述– 時相論理TCTLで検証する特性を記述
2014/09/01

SES2014チュートリアル

12
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

本チュートリアルの概要
 はじめに – モデル検査とは– 形式⼿法とは？

› どんな⼿法がある？
› どんなツールがある？

 組込みソフトウェア開発への導⼊事例– モデル検査の導⼊事例– そのほかの形式⼿法の導⼊事例

 モデル検査によるUML設計検証⽀援ツール– ツールの概要› ツールを利⽤するための準備› ツールの使い⽅について– 適⽤事例
2014/09/01

SES2014チュートリアル

13
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

モデル検査の導⼊事例
 SPIN– ⽇⽴ソリューション社，Blu‐Rayディスク制御ミドルウェア– Selex Communications社，船舶通信システム

 FDR– Philips Healthcare社，X線CTスキャンシステムの制御ソフトウェア

 VDM‐Tools– フェリカネットワークス社，Felicaチップ

 UPPAAL– JAXA，実⾏衛星の姿勢制御ソフトウェア
2014/09/01

SES2014チュートリアル

14
Circuit Design Engineering Lab. ‐ Okayama Prefectural University定理証明の導⼊事例
PVS– Logica Nederland B.V.社，運河の⽔⾨開閉の意
志決定システム› 仕様記述にはZを導⼊› 制御構造の検証にSPINを導⼊

2014/09/01

SES2014チュートリアル

15
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

形式仕様記述の導⼊事例
 Z記法– Praxis社，航空管制システムiFACT– PMES社等，艦載ヘリコプタ運⾏システム

 B, Event‐B– STS社，地下鉄列⾞制御システム– ClearSy社，地下鉄プラットフォームドア制御システ
ム

 CSP

– Altran Praxis社，ICカード認証システム

 SCADE– Airbus社，航空制御システム– POSCON社，地下鉄プラットフォームドア制御システ
ム
2014/09/01

SES2014チュートリアル

16
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

本チュートリアルの概要
 はじめに – モデル検査とは– 形式⼿法とは？

› どんな⼿法がある？
› どんなツールがある？

 組込みソフトウェア開発への導⼊事例– モデル検査の導⼊事例– そのほかの形式⼿法の導⼊事例

 モデル検査によるUML設計検証⽀援ツール– ツールの概要› ツールを利⽤するための準備› ツールの使い⽅について– 適⽤事例
2014/09/01

SES2014チュートリアル

17
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

検証⽀援ツール モデル検査の導⼊コスト削減を⽬的として，
IPA/SECが実施した2013年度RISE事業の⽀援を受けて開発
 UMLの状態マシン図・シーケンス図による設計を対象
 モデル検査ツールNuSMVで検証を
⾏うための⼊⼒モデルを⾃動⽣成 現在のバージョンはコマンドラインでの動作のみをサポート
 当研究室のWebサイトにて公開中– http://circuit.cse.oka‐pu.ac.jp/tool.html

2014/09/01

SES2014チュートリアル

18
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

概要

記述制約
UML図

UMLモデリングツール
astah*

検証モデル(*.smv)

検証結果(*.out)モデル検査ツール
NuSMV

出⼒インタフェース

要求仕様

抽象化・変換モジュール

UML図(*.asta)

⼊⼒インタフェース

要求仕様(*.ctl)仕様
テンプレート

検証結果(整形済)(*.result)

違反箇所
情報(*.ce)

検証⽀援ツール
外部ツール

 UML図の記述にはastah*を，検証にはNuSMVを⽤いる UML図が満たすべき記述制約と，要求仕様を記述するための仕様テンプレートが定められている
2014/09/01

SES2014チュートリアル

19Circuit Design Engineering Lab. ‐ Okayama Prefectural University

検証モデル⽣成の流れ
MODULE main
VAR
XXX : {aaa, bbb, ccc};
YYY : {ddd, eee, fff};
fg1 : boolean;

モデル⽣成

状態マシン図モデル

init(YYY) := ddd;
next(YYY) := casefg = FALSE : fff
TRUE : YYY;
esac;

シーケンス図
UML図ファイル(*.asta)safe(xxx = 1)live(message_1)
reachable(S)
要求仕様ファイル(*.ctl)
2014/09/01

ASSIGNinit(XXX) := aaa;
next(XXX) := casefg = TRUE : bbb;
TRUE : XXX;
esac;

CTL式
⽣成

init(fg) := FALSE;
next(fg) := casefg = FALSE : {TRUE, FALSE};
TRUE : fg;
esac;
SPEC AG !(XXX = ccc)
SPEC EF(ZZZ = iii)
SPEC AF(YYY = fff)

CTL式

検証モデルファイル(*.smv)

SES2014チュートリアル

20
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

ツールの導⼊準備
対象OS– Windows7(64bit), Windows8(64bit), Mac OS 10.7

実⾏環境
– Java 7のインストール– astah* community 6.7のインストール– NuSMV 2.5.4のインストール– 検証⽀援ツールのインストール› ダウンロードして解凍

2014/09/01

SES2014チュートリアル

21
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

ツールの使い⽅
1. UMLモデルの作成(astah*)
2. 要求仕様の記述(テキストエディタ)
3. SMVファイルの⽣成(検証⽀援ツール)
4. SMVファイルの修正(テキストエディタ)
5. モデル検査の実⾏(NuSMV)
6. 検査結果の整形(検証⽀援ツール)

2014/09/01

SES2014チュートリアル

22
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

UMLモデルの作成
astah*を⽤いて作成– 状態マシン図・シーケンス図が対象

記述制約– 状態マシン図› 単純状態およびその遷移のみを扱う› 変数は整数型・ブール型のみを扱う– シーケンス図› 結合フラグメントによる階層構造をもたない，単純な相互作⽤のみを扱う

2014/09/01

SES2014チュートリアル

23
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

要求仕様の記述
 仕様テンプレートを⽤いて記述する

 直接記述することも可能– NuSMVにおける⼊⼒形式であるCTLで記述する› CTL：時相論理の⼀種
2014/09/01

SES2014チュートリアル

24
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

SMVファイルの⽣成
UML図(*.asta)と要求仕様(*.ctl)を⼊⼒としてSMVファイル(*.smv)を⽣成する
java –jar umltool.jar UML図ファイル名.asta 要求仕様ファイル名.ctl– SMVファイルの拡張⼦を除いたファイル名は，UML図ファイル名と同じものとなる

2014/09/01

SES2014チュートリアル

25
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

SMVファイルの修正
本ツールで⽣成されたSMVファイルでは，変数の初期値および定義域は記述されていない– 状態マシン図において，これらを直接記述するための記法が存在しないため

ユーザが記述する必要がある
VAR

VAR

X : 型を⼊⼒してください
Y : 型を⼊⼒してください

X : {1, 3, 5};
Y : 0..10;

2014/09/01

SES2014チュートリアル

26
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

モデル検査の実⾏修正したSMVファイル(*.smv)を⼊⼒としてNuSMVによるモデル検査を⾏い，結果を検証結果ファイル(*.out)を保存する
NuSMV.exe –coi SMVファイル名.smv > 検証結果ファイル名.out– coi(Cone of Influence)は，要求仕様と不要なモデルを抽象化し，検証を⾼速化するためのオプション

2014/09/01

SES2014チュートリアル

27
Circuit Design Engineering Lab. ‐ Okayama Prefectural University検証結果の整形検証結果ファイル(*.out)を⼊⼒として，整形済み検証結果ファイル(*.result)と反例ファイル(*.ce)を⽣成する
java –jar umltool.jar 検証結果ファイル名.out– 整形済み検証結果ファイルと反例ファイルの拡張⼦を除いたファイル名は，検証結果ファイル名と同じものとなる– 検証の結果として全ての要求仕様が満たされた場合，反例ファイルは⽣成されない
2014/09/01

SES2014チュートリアル

28
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

事例適⽤による評価
 経緯– 某ソフトウェア開発企業に事例提供を打診– 開発に⽤いた状態遷移表からUML図(状態マシン図)を作成– 対象システムは店舗従業員向けの「商品供給指⽰システム」› 売場の端末と商品管理室のモニタの間で，商品供給のための通信を⾏う 検査項⽬– 検査１：仕様テンプレートを⽤いた基本特性の検査– 検査２：事例提供元より要望のあった特性の検査

2014/09/01

SES2014チュートリアル

29
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

対象となるUML図
2台の売場端末とモニター表⽰の動作の状態マシン図(状態遷移表を元に作成)

端末A

モニター
2014/09/01

SES2014チュートリアル

端末B

UML図ファイル
R_CDS.asta30Circuit Design Engineering Lab. ‐ Okayama Prefectural University

売場端末の振る舞い
各端末は4つの状態をもつ– 待機中(wait)，発話中(send)，着信中(receive)，通話中(com)同時に2回線(MD=2)まで通話が可能

2014/09/01

SES2014チュートリアル

31
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

管理室モニタの振る舞い
通話回線数に応じて6つの状態をもつ– surplus(0)，sufficient(1)，optimal(2)，few(3)，short(4)，non_plot(不明)通話回線数は端末AおよびBの通話回線数の和(MD_A + MD_B)となる

2014/09/01

SES2014チュートリアル

32
Circuit Design Engineering Lab. ‐ Okayama Prefectural University検証する特性（検査１）仕様テンプレートを⽤いて４つの基本特性を記述
検査項⽬

状態の到達可能性

通信モードの到達可能性

通信モードの安全性モニターの到達可能性

2014/09/01

テンプレートreachable(s)reachable(x,a)

ツールへの⼊⼒
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(MD_A, 1)
reachable(MD_A, 2)
reachable(MD_B, 1)
reachable(MD_B, 2)
safe(MD_A, 3)safe(MD_A, ‐1)safe(x,a)

要求仕様
ファイル
BASIC.ctl

safe(MD_B, 3)safe(MD_B, ‐1)reachable(s)reachable(Ctl_Monitor = surplus)
reachable(Ctl_Monitor = sufficient)reachable(Ctl_Monitor = optimal)reachable(Ctl_Monitor = few)
reachable(Ctl_Monitor = short)

SES2014チュートリアル

33
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/09/01

誤りは存在しない

SES2014チュートリアル

34
Circuit Design Engineering Lab. ‐ Okayama Prefectural University検証する特性（検査２）
事例提供元より要望のあった特性を直接検査式として記述
1.
2.
3.

端末が待機状態であり，かつ通信モードが通話無しでない状態への到達可能性
端末が着信中状態であり，かつ通信モードが2回線通話である状態への到達可能性
端末が通話中であり，かつ通信モードが通話無しである状態への到達可能性

1A: SPEC !EF(Terminal_A = wait & !(MD_A = 0))
2A: SPEC !EF(Terminal_A = receive & MD_A = 2)
3A: 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/09/01

SES2014チュートリアル

要求仕様ファイル
R_CDS_REQ.ctl

35
Circuit Design Engineering Lab. ‐ Okayama Prefectural University検証結果（検査２）
R_CDS.asta
R_CDS_REQ.ctl(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.smv

R_CDS_REQ.out

R_CDS_REQ.result
R_CDS_REQ.ce

3A,3Bの結果がFALSE

誤りを検出し，反例を出⼒(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/09/01

SES2014チュートリアル

36
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

⽣成された検証結果ファイル

R_CDS_REQ.result

R_CDS_REQ.ce
2014/09/01

SES2014チュートリアル

37
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

反例の解析
特性3Aに対する反例の解析(3Bも同様)
1

2

3

45

Event_A

emp

emp

reportresponse

emp

MD_A00000

Terminal_A

initialinitialwait

sendcom

端末が通信中(Terminal_A=com)であるにもかかわらず，通信モードが通話無し(MD_A=0)となる状態に到達している原因：状態遷移表のアクションの１つがUML図に正しく転記されていなかった• UML図による設計の誤りを正しく検出できた• 反例を元に誤り箇所を特定することができた
2014/09/01

SES2014チュートリアル

38
Circuit Design Engineering Lab. ‐ Okayama Prefectural Universityまとめモデル検査とは？
– 形式⼿法の⼀種– ⾃動的かつ網羅的検証が可能な技術

形式⼿法とは？
– 形式仕様記述と形式的証明

形式⼿法の適⽤事例– 交通・医療に関して多くの事例

検証⽀援ツールの紹介
2014/09/01

SES2014チュートリアル

39
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

SESワークショップのお知らせ
SES2014のワークショップにて，形式⼿法に関するセッションを開催します
形式⼿法 ‐ 産学連携における問題とその解決 –討論リーダ：横川智教（岡⼭県⽴⼤）早⽔公⼆（フォーマルテック）
⽇時・場所：9⽉3⽇(⽔) 10:20〜
3F 302室
興味のある⽅は是⾮お越しください
2014/09/01

SES2014チュートリアル

40
Circuit Design Engineering Lab. ‐ Okayama Prefectural University

謝辞
本チュートリアルの⼀部は，
独⽴⾏政法⼈情報処理推進機構・技術本部
ソフトウェア⾼信頼化センター(IPA/SEC)が実施した，「2013年度ソフトウェア⼯学分野の先導的研究⽀援事業(RISE)」の⽀援を受けています．

2014/09/01

SES2014チュートリアル

41
Circuit Design Engineering Lab. ‐ Okayama Prefectural University