Microsoft PowerPoint SES2014.pptx

Size: px

Start display at page:

Download "Microsoft PowerPoint SES2014.pptx"

いぶきかがんじ
5 years ago
Views:

1 組込みソフトウェア検証へのモデル検査技術の導に関する技術動向横川智教 t yokoga@cse.oka pu.ac.jp 岡県学

2 講師紹介所属岡県学情報学部情報システム学科回路デザイン研究室助教最近の研究テーマモデル検査による組込みソフトウェアの設計検証同期回路のモデル化性能評価検証連絡先 t yokoga@cse.oka pu.ac.jp pu.ac.jp/ 2014/09/01 SES2014 チュートリアル 2

3 本チュートリアルの概要はじめにモデル検査とは形式法とは? どんな法がある? どんなツールがある? 組込みソフトウェア開発への導事例モデル検査の導事例そのほかの形式法の導事例モデル検査による UML 設計検証援ツールツールの概要ツールを利するための準備ツールの使いについて適事例 2014/09/01 SES2014 チュートリアル 3

4 本チュートリアルの概要はじめにモデル検査とは形式法とは? どんな法がある? どんなツールがある? 組込みソフトウェア開発への導事例モデル検査の導事例そのほかの形式法の導事例モデル検査による UML 設計検証援ツールツールの概要ツールを利するための準備ツールの使いについて適事例 2014/09/01 SES2014 チュートリアル 4

5 モデル検査形式法 (formal method) の種システムの動検証技術システムを状態遷移グラフでモデル化し, モデルの網羅的探索によって求める特性を満たすか否かを動的に判定に到達することはできるか? からは必ずに到達するか? 状態遷移グラフ 2014/09/01 SES2014 チュートリアル 5

6 形式法形式法とはシステム開発に数学論理学を導するための技術続きの動化による品質向上コスト削減形式法の利仕様記述集合論に基づいてデータ構造を記述述語論理をいてシステムの要求を表現開発プロセス代数論により要求と設計の等価性判定検証公理によるプログラム証明グラフ探索アルゴリズムによる特性検証 2014/09/01 SES2014 チュートリアル 6

7 主な形式法形式仕様記述 (formal specification) システムの仕様を集合論や論理式をいて数学的に表現するための記法抽象的かつ厳密な記述形式的証明 (formal reasoning) 形式的な続きに基づいてシステムの正しさを証明するための技術定理証明とモデル検査に分類される 2014/09/01 SES2014 チュートリアル 7

8 形式的証明定理証明 (theorem proving) 公理と推論規則に基づいてシステムの性質を証明完全に動化することは困難とされる証明の動成を援するツールは存在モデル検査 (model checking) 状態遷移グラフでモデル化されたシステムの網羅的探索に基づいて求める性質を満たすか検証完全に動化された続き有限状態システムのみが対象状態爆発への対処が課題 2014/09/01 SES2014 チュートリアル 8

9 主な形式仕様記法 Z 集合論, 述語論理,λ 計算の記法に基づいてプログラムの仕様と振る舞いを記述する B, Event B 段階的詳細化により仕様記述からプログラム成をう法 (B メソッド ) においていられる CSP プロセス代数論に基づいて, 並動作するプロセス群の相互作を記述する SCADE 同期型プログラミング語であり, 時間に同期して動作するリアルタイムシステムの記述が可能 2014/09/01 SES2014 チュートリアル 9

10 主な定理証明援ツール PVS 集合論に基づく仕様記述語と検証ツールによって構成対話的な定理証明が可能 Coq 定理証明援語 Coq 語で記述したプログラムに対する証明が可能 2014/09/01 SES2014 チュートリアル 10

11 主なモデル検査ツール (1) SPIN 分散システムを対象としたモデル検査ツール時相論理 LTL で検証する特性を記述システムと特性をオートマトンでモデル化 FDR CSP モデルを対象としたモデル検査ツールプロセスの模倣性検証が可能 VDM Tools 形式仕様記法 VDM SL,VDM++ で記述された仕様の検証や実が可能 2014/09/01 SES2014 チュートリアル 11

12 主なモデル検査ツール (2) SMV 記号モデル検査アルゴリズムに基づいた速な検証が可能専語 (SMV 語 ) で検査対象システムを記述時相論理 CTL で検証する特性を記述 UPPAAL リアルタイムシステムを対象としたモデル検査ツール時間オートマトンで検査対象システムを記述時相論理 TCTL で検証する特性を記述 2014/09/01 SES2014 チュートリアル 12

13 本チュートリアルの概要はじめにモデル検査とは形式法とは? どんな法がある? どんなツールがある? 組込みソフトウェア開発への導事例モデル検査の導事例そのほかの形式法の導事例モデル検査による UML 設計検証援ツールツールの概要ツールを利するための準備ツールの使いについて適事例 2014/09/01 SES2014 チュートリアル 13

14 モデル検査の導事例 SPIN ソリューション社,Blu Ray ディスク制御ミドルウェア Selex Communications 社, 船舶通信システム FDR Philips Healthcare 社,X 線 CT スキャンシステムの制御ソフトウェア VDM Tools フェリカネットワークス社,Felica チップ UPPAAL JAXA, 実衛星の姿勢制御ソフトウェア 2014/09/01 SES2014 チュートリアル 14

15 定理証明の導事例 PVS Logica Nederland B.V. 社, 運河の開閉の意志決定システム仕様記述にはZを導制御構造の検証にSPINを導 2014/09/01 SES2014 チュートリアル 15

16 形式仕様記述の導事例 Z 記法 Praxis 社, 航空管制システム ifact PMES 社等, 艦載ヘリコプタ運システム B, Event B STS 社, 地下鉄列制御システム ClearSy 社, 地下鉄プラットフォームドア制御システム CSP Altran Praxis 社,IC カード認証システム SCADE Airbus 社, 航空制御システム POSCON 社, 地下鉄プラットフォームドア制御システム 2014/09/01 SES2014 チュートリアル 16

17 本チュートリアルの概要はじめにモデル検査とは形式法とは? どんな法がある? どんなツールがある? 組込みソフトウェア開発への導事例モデル検査の導事例そのほかの形式法の導事例モデル検査による UML 設計検証援ツールツールの概要ツールを利するための準備ツールの使いについて適事例 2014/09/01 SES2014 チュートリアル 17

18 検証援ツールモデル検査の導コスト削減を的として, IPA/SECが実施した2013 年度 RISE 事業の援を受けて開発 UMLの状態マシン図シーケンス図による設計を対象モデル検査ツールNuSMVで検証をうためのモデルを動成現在のバージョンはコマンドラインでの動作のみをサポート当研究室のWebサイトにて公開中 pu.ac.jp/tool.html 2014/09/01 SES2014 チュートリアル 18

19 概要要求仕様 (*.ctl) UML 図 (*.asta) 2014/09/01 SES2014チュートリアル 19 astah* スUML モデリングツールインタフェー仕様テンプレート要求仕様記述制約 UML 図抽象化変換モジュール検証モデル (*.smv) 検証結果 (*.out) モデル検査ツール NuSMV 検証結果 ( 整形済 ) (*.result) 違反箇所情報 (*.ce) ス検証援ツール出インタフェー外部ツール UML 図の記述にはastah* を, 検証にはNuSMVをいる UML 図が満たすべき記述制約と, 要求仕様を記述するための仕様テンプレートが定められている

20 検証モデル成の流れ 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; UML 図ファイル (*.asta) safe(xxx = 1) live(message_1) reachable(s) 要求仕様ファイル (*.ctl) 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) 検証モデルファイル (*.smv) CTL 式 2014/09/01 SES2014 チュートリアル 20

21 ツールの導準備対象 OS Windows7(64bit), Windows8(64bit), Mac OS 10.7 実環境 Java 7のインストール astah* community 6.7のインストール NuSMV 2.5.4のインストール検証援ツールのインストールダウンロードして解凍 2014/09/01 SES2014 チュートリアル 21

22 ツールの使い 1. UMLモデルの作成 (astah*) 2. 要求仕様の記述 ( テキストエディタ ) 3. SMVファイルの成 ( 検証援ツール ) 4. SMVファイルの修正 ( テキストエディタ ) 5. モデル検査の実 (NuSMV) 6. 検査結果の整形 ( 検証援ツール ) 2014/09/01 SES2014 チュートリアル 22

23 UML モデルの作成 astah* をいて作成状態マシン図シーケンス図が対象記述制約状態マシン図単純状態およびその遷移のみを扱う変数は整数型ブール型のみを扱うシーケンス図結合フラグメントによる階層構造をもたない, 単純な相互作のみを扱う 2014/09/01 SES2014 チュートリアル 23

24 要求仕様の記述仕様テンプレートをいて記述する直接記述することも可能 NuSMV における形式である CTL で記述する CTL: 時相論理の種 2014/09/01 SES2014 チュートリアル 24

25 SMV ファイルの成 UML 図 (*.asta) と要求仕様 (*.ctl) をとして SMV ファイル (*.smv) を成する java jar umltool.jar UML 図ファイル名.asta 要求仕様ファイル名.ctl SMV ファイルの拡張を除いたファイル名は, UML 図ファイル名と同じものとなる 2014/09/01 SES2014 チュートリアル 25

26 SMV ファイルの修正本ツールで成された SMV ファイルでは, 変数の初期値および定義域は記述されていない状態マシン図において, これらを直接記述するための記法が存在しないためユーザが記述する必要がある VAR X : 型をしてください Y : 型をしてください VAR X : {1, 3, 5}; Y : 0..10; 2014/09/01 SES2014 チュートリアル 26

27 モデル検査の実修正した SMV ファイル (*.smv) をとして NuSMV によるモデル検査をい, 結果を検証結果ファイル (*.out) を保存する NuSMV.exe coi SMV ファイル名.smv > 検証結果ファイル名.out coi(cone of Influence) は, 要求仕様と不要なモデルを抽象化し, 検証を速化するためのオプション 2014/09/01 SES2014 チュートリアル 27

28 検証結果の整形検証結果ファイル (*.out) をとして, 整形済み検証結果ファイル (*.result) と反例ファイル (*.ce) を成する java jar umltool.jar 検証結果ファイル名.out 整形済み検証結果ファイルと反例ファイルの拡張を除いたファイル名は, 検証結果ファイル名と同じものとなる検証の結果として全ての要求仕様が満たされた場合, 反例ファイルは成されない 2014/09/01 SES2014 チュートリアル 28

29 事例適による評価経緯某ソフトウェア開発企業に事例提供を打診開発にいた状態遷移表から UML 図 ( 状態マシン図 ) を作成対象システムは店舗従業員向けの商品供給指システム売場の端末と商品管理室のモニタの間で, 商品供給のための通信をう検査項検査 1: 仕様テンプレートをいた基本特性の検査検査 2: 事例提供元より要望のあった特性の検査 2014/09/01 SES2014 チュートリアル 29

30 対象となる UML 図 2 台の売場端末とモニター表の動作の状態マシン図 ( 状態遷移表を元に作成 ) 端末 A 端末 B モニター UML 図ファイル R_CDS.asta 2014/09/01 SES2014 チュートリアル 30

31 売場端末の振る舞い各端末は 4 つの状態をもつ待機中 (wait), 発話中 (send), 着信中 (receive), 通話中 (com) 同時に 2 回線 (MD=2) まで通話が可能 2014/09/01 SES2014 チュートリアル 31

32 管理室モニタの振る舞い通話回線数に応じて 6 つの状態をもつ surplus(0),sufficient(1),optimal(2),few(3),short(4), non_plot( 不明 ) 通話回線数は端末 A および B の通話回線数の和 (MD_A + MD_B) となる 2014/09/01 SES2014 チュートリアル 32

33 検証する特性 ( 検査 1) 仕様テンプレートをいて 4 つの基本特性を記述検査項テンプレートツールへの状態の到達可能性通信モードの到達可能性通信モードの安全性 reachable(s) reachable(x,a) safe(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(md_b, 3) safe(md_b, 1) 要求仕様ファイル BASIC.ctl モニターの到達可能性 reachable(s) reachable(ctl_monitor = surplus) reachable(ctl_monitor = sufficient) reachable(ctl_monitor = optimal) reachable(ctl_monitor = few) reachable(ctl_monitor = short) 2014/09/01 SES2014 チュートリアル 33

34 検証結果 ( 検査 1) R_CDS.asta BASIC.ctl R_CDS_BASIC.smv R_CDS_BASIC.out R_CDS_BASIC.result 本ツールをいて SMV ファイルを成モデル検査器 NuSMV で検査検査結果の整形 (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 全ての結果が TRUE 誤りは存在しない 2014/09/01 SES2014 チュートリアル 34

35 検証する特性 ( 検査 2) 事例提供元より要望のあった特性を直接検査式として記述 1. 端末が待機状態であり, かつ通信モードが通話無しでない状態への到達可能性 2. 端末が着信中状態であり, かつ通信モードが 2 回線通話である状態への到達可能性 3. 端末が通話中であり, かつ通信モードが通話無しである状態への到達可能性 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) 要求仕様ファイル R_CDS_REQ.ctl 2014/09/01 SES2014 チュートリアル 35

36 検証結果 ( 検査 2) 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( 部 ) 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

37 成された検証結果ファイル R_CDS_REQ.result R_CDS_REQ.ce 2014/09/01 SES2014 チュートリアル 37

38 反例の解析特性 3A に対する反例の解析 (3B も同様 ) Event_A emp emp report response emp MD_A Terminal_A initial initial wait send com 端末が通信中 (Terminal_A=com) であるにもかかわらず, 通信モードが通話無し (MD_A=0) となる状態に到達している原因 : 状態遷移表のアクションの 1 つが UML 図に正しく転記されていなかった UML 図による設計の誤りを正しく検出できた反例を元に誤り箇所を特定することができた 2014/09/01 SES2014 チュートリアル 38

39 まとめモデル検査とは? 形式法の種動的かつ網羅的検証が可能な技術形式法とは? 形式仕様記述と形式的証明形式法の適事例交通医療に関して多くの事例検証援ツールの紹介 2014/09/01 SES2014 チュートリアル 39

40 SES ワークショップのお知らせ SES2014 のワークショップにて, 形式法に関するセッションを開催します形式法産学連携における問題とその解決討論リーダ : 横川智教 ( 岡県 ) 早公 ( フォーマルテック ) 時場所 :9 3 ( ) 10:20 3F 302 室興味のあるは是お越しください 2014/09/01 SES2014 チュートリアル 40

41 謝辞本チュートリアルの部は, 独政法情報処理推進機構技術本部ソフトウェア信頼化センター (IPA/SEC) が実施した, 2013 年度ソフトウェア学分野の先導的研究援事業 (RISE) の援を受けています. 2014/09/01 SES2014 チュートリアル 41

2013 年年度度ソフトウェア工学分野の先導的研究支援事業抽象化に基づいた UML 設計の検証支援ツールの開発公立立大学法人岡山県立立大学情報工学部情報システム工学科横川智教 Circuit Design Engineering Lab. - Okayama Prefec

2013 年年度度ソフトウェア工学分野の先導的研究支援事業抽象化に基づいた UML 設計の検証支援ツールの開発公立立大学法人岡山県立立大学情報工学部情報システム工学科横川智教 Circuit Design Engineering Lab. - Okayama Prefec 2013 年年度度ソフトウェア工学分野の先導的研究支援事業抽象化に基づいた UML 設計の検証支援ツールの開発公立立大学法人岡山県立立大学情報工学部情報システム工学科横川智教背景 - 組込みソフトウェア開発の課題組込みソフトウェアの開発プロセス要求分析設計実装テスト手戻り下流流工程での不不具合の検出上流流工程への手戻りの発生手戻りによる開発コスト増