同時性を考慮した振舞い検証手法 - アーキテクチャ指向形式手法に基づく

同時性を考慮した振舞い検証手法
張漢明
南山大学理工学部ソフトウェア工学科
発表内容
✓ 研究の背景と目的
✓ 区間の概念を用いた振舞い記述法
✓ 振舞い検証の枠組み
✓ 事例：自動販売機システム
✓ 考察
✓ 開発文書の体系
2
研究の背景と目的
組込みシステムの基本構造
センサ
アクチュ
エータ
センサ
アクチュ
エータ
制御
アクチュ
エータ
センサ
問題が起こるのは？
同時に複数の事象が起こった場合
漏れなく事象を検知！
4
2つのセンサ制御
センサ1
センサ2
1 事象
事象 2
センサ1
制御
センサ2
制御
事象 3
4 事象
制御
分散して起こる事象を逐次プロセスで制御
同時に事象が起こるという記述が必要
5
非同期通信
際どいタイミング（1）
制御
センサ制御
ハードウェア
sense
off
sense
off
ok
6
非同期通信
際どいタイミング（2）
制御
センサ制御
ハードウェア
off
sense
off
ok
sense
テストで検証することは（ほぼ）不可能
7
モデル検査
✓ 全ての有限状態を網羅的に調べて，仕様を自動的に調
べる技術
-
状態に基づくモデル検査器　（Spin）
-
-
時相論理式
事象に基づくモデル検査器　（CSP/FDR）
-
プロセス代数　（事象の振舞い等価性）
正しい仕様をどのように記述するか？
8
研究の目的
本研究の目的は，複数事象発生の同時性を考慮した，
並行システム設計の検証を支援することである．
✓ 振舞い仕様記述法の提案
-
同時性の定義
-
同時の振舞いを簡潔に記述
✓ 振舞い検証の枠組みの提案
-
振舞い仕様の再利用性の向上
9
基本的なアイデア
✓ 振舞い仕様記述法
-
振舞いを区間の合成で表現
-
同時性を区間内に局所化
✓ 振舞い検証の枠組み
-
振舞い仕様の事象を環境に局所化
-
制約による振舞いの限定
✓ 意味を形式言語で定義
10
CSP
✓ Communicating
Sequential Processes
✓ 並行システムを記述・検証するための言語
-
逐次プロセス
-
並行プロセス
✓ 対象と仕様を同じ言語で記述
✓ FDR
-
CSP の最も代表的なモデル検査器
11
区間の概念を用いた振舞い仕様記述法
区間
✓ 単純区間
✓ 複合区間
-
区間の基本単位
-
区間の合成
-
複数の事象
-
逐次，並行
13
単純区間の振舞い
開始終了付き事象
単純区間
14
単純区間（CSP）
開始終了付き事象
EVENT_WITH_START_AND_END(start,end,event) =
start ->
(event -> end -> SKIP [] end -> SKIP)
単純区間
SIMPLE_SECTION(s) =
||| (start, end, event):s @
EVENT_WITH_START_AND_END(start, end, event)
s: 開始終了付き事象（3項組）の集合
15
複合区間
✓ 合成演算子
-
逐次　;
-
選択　[]
-
並行　|||
-
再帰
P = A; ((X1; X2) ||| Y); P
16
区間内の事象発生
✓ 単一事象選択
-
区間で定義されている事象のうち，任意の1つの事象
が発生する
✓ 複数事象発生
-
区間で定義されている事象のうち，指定した複数の
事象が発生する
17
区間内の事象発生
単一事象選択
SEL_SECTION(s) =
[] event:OccurredEvents(s) @ event -> SKIP
OccurredEvents(s) = {event | (start, end, event) <- s}
複数事象発生
PL_SECTION(occurred, not_occurred) =
(||| (st, end, ev):occurred @ st -> ev -> end -> SKIP)
|||
(||| (st, end, ev):not_occurred @ st -> end -> SKIP)
18
振舞い検証の枠組み
CSP による検証
✓ デッドロックフリー
✓ ライブロックフリー
✓ 詳細化関係（Refinement）　仕様
[= 実現
-
Trace Model　（安全性検証）
-
Failures Model　（活性検証）
-
Failures-Divergences Model　（内部イベントのループ）
✓ 等価性
-
仕様 [= 実現　かつ　実現 [= 仕様
20
検証の枠組み
システム　＝　検証の対象　||　環境
環境：システムの外部インターフェース
検証　＝　システムの入力に対して仕様を満たす
仕様：入出力関係
システムの振舞い
制約
入力
21
検証の枠組み　（CSP）
システム = 検証の対象 [|SYN_ENV|] 環境
検証　＝　仕様　[=　TARGET(実現，着目する事象）
TARGET(S, targets) = S ＼ diff(Events, targets)
実現　＝　CONSTRAINT(システム，SYN，入力）
CONSTRAINT(p, sync, c) = p [|sync|] c
区間を用いた入力
CONSTRAINT(システム, SYN_SEC, 区間）
22
事例：自動販売機システム
自動販売機
/ C <- on
24
ナイーブな検証
SYSTEM = VM ||| ENV
COMP = VM ||| COIN ||| BUTTON ||| LEVER ||| ITEM ||| CHANGE
ENV = E_COIN ||| E_BUTTON ||| E_LEVER ||| E_ITEM ||| E_CHANGE
SYSTEM :[ deadlock free [F] ]
25
区間を用いた入力の振舞い
SECTION_MODEL = CONSTRAINT(SYSTEM, SYN_SEC, INPUT)
INPUT = DEPOSIT; SELECT; INPUT
DEPOSIT = SIMPLE_SECTION({COIN})
SELECT = SIMPLE_SECTION({BUTTON, LEVER})
COIN = (env_ev.Coin.on, env_ev.Coin.off,　send.Coin.inserted)
BUTTON = (env_ev.Button.on, env_ev.Button.off, send.Button.pushed)
LEVER = (env_ev.Lever.on, env_ev.Lever.off, send.Lever.inserted)
26
逐次事象の振舞い検証
SEQ_MODEL = CONSTRAINT(SECTION_MODEL, SYN_SEC, SEQ_S)
SEQ_S =
SEL_SECTION({COIN});
SEL_SECTION({BUTTON, LEVER}); SEQ_S
SEQ_MODEL :[ deadlock free [F] ]
SEQ_SPEC =
EXT_INSERTED;
(EXT_PUSHED; EXT_ITEM [] EXT_PULLED; EXT_CHANGE);
EXT_INSERTED = send.Coin.inserted -> SKIP
SEQ_SPEC
EXT_PUSHED = send.Button.pushed -> SKIP
EXT_PULLED = send.Lever.pulled -> SKIP
SEQ_SPEC [FD= TARGET(SEQ_MODEL, ExternalEvents)
27
同時事象を考慮
同時
仕様：ボタンとレバーが同時に起これば購入
28
同時
検証
PL_MODEL =
CONSTRAINT(SECTION_MODEL,
ExternalControlEvents, PL)
PL =
PL_SECTION({COIN}, {});
PL_SECTION({BUTTON, LEVER}, {}); PL
PL_SPEC = EXT_INSERTED;
(EXT_PUSHED ||| EXT_PULLED); EXT_ITEM;
PL_SPEC
PL_SPEC [FD= TARGET(PL_MODEL, ExternalEvents)
29
考察
記述の容易性
✓ 振舞い仕様と同期の分離
-
入力に関する同期は区間に局所化
-
振舞い仕様は本質的な事象に限定した記述
IN = c.on -> c.in -> b.on -> b.pushed -> l.on -> l.pulled -> l.off -> IN
IN = c.in -> b.pushed -> l.pulled -> IN
✓ 区間を用いた入力群の記述
IN = c.on -> c.in -> b.on -> b.pushed -> l.on -> l.pulled -> l.off -> IN
IN = c.on -> c.in -> b.on -> l.on -> b.pushed -> l.pulled -> l.off -> IN
IN = c.on -> c.in -> l.on -> b.on -> b.pushed -> l.pulled -> l.off -> IN
:
IN = C_ON; PL_B_PUSHED_L_PULLED; IN
31
記述の再利用性
✓ 入力の振舞いを環境に局所化
-
環境：入出力の外部インターフェース
-
設計を変更しても全く同じ検証式を再利用可能
-
ハードウェアの変更が設計に影響しない
✓ 段階的な設計
-
同時を考慮しない設計
-
-
区間を逐次モデルに制約した検証
同時を考慮した設計
-
同時を考慮しない設計の検証を回帰的に利用
32
まとめ
複数事象発生の同時性を考慮した，並行システム
設計の振舞い検証手法の提案
✓
区間を用いた事象の同時性の定義
-
同時性に関する同期を区間に局所化
-
-
✓
振舞い仕様記述の容易性の向上
振舞いを環境に局所化
-
今後の課題
-
保守性の向上
33
例外処理への適用
仕様の網羅性
非決定性演算子の導入
開発文書の体系
目的
✓ ソフトウェア開発における形式手法技術の実用化
-
現実のソフトウェア開発における形式手法技術の必
要性・有効性・意義を明確化
-
-
適用技術の位置付け
-
何のために何ができるのか
-
「切り口」を明示
最終成果物（プログラム）との関連
-
詳細化（Refinement）を明示
35
システム記述
入力
出力
システム
•
•
システム = 機械の集合
入出力関係を定義
機械
ハードウェア
インター
フェース
36
ソフトウェア
開発文書
要求
開発文書
根拠
文書
仕様
根拠
スコープ
設計
37
詳細化関係
開発文書
要求
詳細化
開発文書
仕様
設計
関係
要求
仕様
38
設計
システム開発
システム開発＝実装可能な設計を含んだ開発文書群の作成
要求
仕様
設計
要求
仕様
設計
詳細化
詳細化
要求
仕様
装置
設計
プログラム
作成
39
図式表現, 自然言語
UML
ハードウェア
Lego
連携
仕様
Z
シミュレーション
Crescendo Tool
アニメーション
Lively Walkthrough
意味（形式記述）
VDM-SL, CSP
関数プログラミング
Haskell
+
語彙
辞書ツール
設計
VDM++
派生開発
フィーチャ
テスト
生成
証明
Coq
モデル検査
Spin
時間
Timed CSP
40

Download Report