![演繹を利用したモデリング
! ? 要求を時相論理式で表現する
! ? 時相論理式から状態マシンを生成する
?uent Moving = <{start},{stop}> initially 0
?uent Closed = <{close},{open}> initially 1
assert AlwaysSafeDoor = [] (Moving->Closed)
constraint LTL01 = AlwaysSafeDoor
open
start
LT L01
0 1 2
{close, stop} {close, start} {open, stop}
stop
close
26](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-26-320.jpg)
![サンプル-1
! ? 水位計の動作モデルを作成せよ
! ? 入力: 水位レベルは0..9まである
! ? level[0..9]
この本に出てくる
演習問題
! ? 出力:
! ? low " "水位レベルが2以下
! ? high
水位レベルが9
! ? normal
LowでもHighでも無い時
28](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-28-320.jpg)
![サンプル-1 解答
! ? 一般的なアブダクション解答
range Level = 0..9
SENSOR = SENSOR[5],
SENSOR[w:Level] = (level[i:Level] -> SENSOR[i]
| when (w<2) low -> SENSOR[w]
| when (w>8) high -> SENSOR[w]
| when (w>=2 && w<=8) normal -> SENSOR[w]
).
level[0..1]
level[9] level[0..1]
AbductionSensor
0 1 2
{level[2..8], normal}
{high, level[9]} {level[0..1], low}
level[2..8] level[9]
level[2..8]
29](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-29-320.jpg)
![サンプル-1 演繹解答
! ? 演繹による解答
?uent Low = <level[0..1],level[2..9]> initially 0
?uent Norm = <level[2..8],{level[0..1],level[9]}> initially 1
?uent High = <level[9], level[0..8]> initially 0
assert LowF = [](low -> Low)
assert NormF = [](normal -> Norm) level[9]
assert HighF = [](high -> High) level[0..1] level[9]
DeductiveSensor
constraint CLowF = LowF 0 1 2
constraint CNormF = NormF
{level[2..8], normal} {level[0..1], low} {high, level[9]}
constraint CHighF = HighF level[2..8] level[0..1]
level[2..8]
minimal ||DeductiveSensor = (CLowF||CNormF||CHighF)
@{high, level[0..9], {low, normal}}.
30](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-30-320.jpg)
! ? [](!Low -> !low)
! ? [](Low -> (low || level[0..1])) ちょっと設計っぽい
! ? 全て同じ状態マシンになる
level[0..1] low アクション
LOW 状態
CLowF
0 1
level[2..9] {level[0..1], low}
Lowが真の状態
level[2..9]
31](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-31-320.jpg)
)
assert T2 = [](ON -> X ((OFF || SCAN || reset) && !BOTTOM))
assert T3 = [](SCAN -> X (OFF || ON || BOTTOM || scan))
assert T4 = [](BOTTOM -> X ((ON || OFF || scan)&& ! SCAN))
assert INIT = (OFF && ! ON && !SCAN && !BOTTOM)
constraint T1 = T1
constraint T2 = T2
constraint T3 = T3
constraint T4 = T4
constraint INIT = INIT
||DeRADIO = (T1||T2||T3||T4||INIT).
35](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-35-320.jpg)
)
! ? BOTTOMでlockはあり得ない
assert T4 = [](BOTTOM -> X ((ON2 || OFF || scan )&& ! SCAN && !lock))
! ? 最低周波数に局があったらどうなるのか、と考えると仕様モレ
39](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-39-320.jpg)
 -> ON)
on
SP01
0 {end, off}
1 {end, lock, on, reset, scan}
off
設計領域の問題なのか要求領域の問題なのか
on状態は複合状態と言うのは設計の発想?
45](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-45-320.jpg)
![排他関係
! ? TUNEDとRESET状態が排他的ならば
! ? assert SP02 = [] ! (TUNED && RESET)
! ? しかし、Top周波数に局があれば排他的にはな
らないのでSP02は不要かも知れない
reset
SP02
0 {lock, off, scan}
1 reset
{off, scan}
46](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-46-320.jpg)
! ? これだと必ず局があることを期待している
! ? scanはend, offでも終了するから
! ? assert SP03 = [](SCAN -> X ( TRUEND || end || off))
SP03
scan
0 {end, lock, off, reset}
1
{end, lock, off, reset}
47](https://image.slidesharecdn.com/random-130124093413-phpapp02/85/-47-320.jpg)
数理的に组み込みソフトを开発する方法入门
- 1. 数理的に組み込みソフトを 開発する方法入門 藤倉俊幸 @tfujikura 2013.1.24
- 2. 自己紹介 ! ? 組込エンジニアです ! ? RTOSとか作っていました ! ? 今の仕事はコンサルです ! ? 時々、インタフェース誌に記事を書いています 2
- 3. 今宵の话题 3
- 4. 論理的アプローチとは ! ? （正しいと考えられた）前提から結論を導き出す手順が明 確になっているアプローチ ! ? ただの依存関係ではない ! ? 論理的な推論によって前提から結論を導出する手順 ! ? アプローチ自身が正しいことを保証されたアプローチ ! ? ただし、結論の正しさは前提に依存する ! ? 自明なことを組み合わせて、正しい結論に到達するプ ロセス 4
- 5. ソフト開発で利用される推論 ! ? 最終的には要求を満たす実装を得ることがソフト 開発の目的 ! ? その過程で複数のタイプの推論が繰り返しおこな われる ! ? 要求から設計、設計から実装を導くあるいは 考え出す時の推論 ! ? 実装が設計を満たしているか、設計が要求 を満たしているか確認する際の推論 5
- 6. 推論タイプによる前提と結論の違い PとQを任意の命題としたときの推論タイプと結論の出し方 仮説形成またはアブダクション(abduction) ! ? QとP?Qが正しい時、Pも正しい ! ? 推論構造として問題がある。P?QをQ?Pの様に使用することが問題。 帰納(induction) ! ? PとQが正しい時、P?Qも正しい ! ? ある事例から規則?法則を帰納して、別の事例を説明する。 ! ? 網羅性が問題となる 演繹(deduction) ! ? PとP?Qが正しい時、Qも正しい ! ? 論理的に正しい推論 6
- 7. 演绎とアブダクション 演繹の例 アブダクションの例 ! ? 天王星の軌道をニュートン ! ? 水星の軌道をニュートン力 力学では説明できなかった。 学で説明するためには、内 説明するためには別の天体 側に別の天体が必要だった。 の存在が必要だった。 ! ? 別の天体は発見されなかっ た。(演繹失敗) ! ? 存在すべき位置を観測した 結果、海王星が発見された。 ! ? 新しい発想に基づく一般相 対性理論によって説明する ! ? 仮説に基づいて海王星の ことができた。 位置を演繹して発見した 7
- 8. 理想の開発スタイル 要求 システムテスト 設計 結合テスト 要求 実装 普通 設計 要求 システムテスト 実装 設計 結合テスト 実装 アブダクション 帰納 形式検証付き 演繹 8
- 9. たとえば 1からnまでの整数の 和を求める この公式を 利用することを思い付く n(n + 1) 2 #defineで充分だろうと思う #define sum(n) (n*(n+1)/2)) アブダクション、発明?発見、思い付き、思考整理など 帰納 演繹 検証、確認など 9
- 10. 演绎とアブダクションの併用 ! ? もの作りの本質はアブダクション ! ? 演繹では新しいことは出てこない ! ? 演繹は既にあるものの形を変えて見せてくれる ! ? 特に動作要求から状態マシン生成 ! ? 要求文à?论理式à?状态マシン 演繹だけだとこんな感じ 結局もとに戻るだけ ! ? 文章がそれと等価な状態マシンになる しかし、ちゃんと戻れることが重要で 正しいことの証明になる ! ? 演繹を利用することで ! ? 信頼性の確保 ! ? 開発効率の向上 10
- 11. たとえば 与えられたa, b, cを三 辺とする三角形を作れ るか判定する 演繹 ヘロンの公式 2s = a + b + cとして s(s – a)(s – b)(s – c) ≧ 0 を確認する ここから先は アブダクションも利用 ??? 11
- 12. 演繹を開発で利用するには ! ? 命題論理を理解する必要がある ! ? 命題論理には既に多くの応用がある ! ? 推論の矛盾の検出と修正 ! ? 原因結果グラフ いきなり命題論理が必要 ! ? FTA と言われた時の騒然とした イメージ ! ? プロダクトラインのフィーチャモデル ! ? プログラムを論理式にしてプログラム検証 ! ? 形式仕様記述 ! ? たとえば、安全要求の導出 12
- 13. たとえば、安全要求 ! ? システムの誤動作によって引き起こされるリスク を回避する ! ? 誤動作 à? ハザード à? リスク ! ? この流れを途中で回避?軽減するための機能 に対する要求が安全要求 ! ? 誤動作を網羅的にリストアップして、リスクに至る ハザードを特定する必要がある 13
- 14. たとえば、エンジン制御 ! ? まず一般的なモデル化をおこなう ! ? 安全要求を導出するだけであれば単純なモデルで充分 ! ? 命題を立てて形式化する U1 エンジン 命題 U3 制御システム U1 : アクセルを踏む U2 : クルーズコントロール U3’ U3 : 加速する U2 U3’: 加速不足 形式化機能モデル: ?U1 ?∨ ?U2∨U3’ ?? ?U3 14
- 15. 误动作の特定 ! ? 機能モデルが偽になって いるところが誤動作 U1 T U2 T U3' T U3 T (U1 ∨ U2∨U3')?U3 T HZ01 HZ02 ? ? ! ? 誤動作とリスクアセスメント T T T T T F F T F T ? ? ? T の結果からリスクに至る誤 T T F F F ? T 動作を特定する T F T T T ? ? T F T F F ? T T F F T T ? ? ! ? リスクに至るハザード T F F F F ? T F T T T T ? ? F T T F F ? T ! ? 意図しないトルク増加 F T F T T ? ? F T F F F ? T F F T T T ? ? U3 ∧￢U1 ∧￢U2 ∧￢U3’ F F T F F ? T F F F T F T ? F F F F T ? ? ! ? 安全目標 ! ? これを防ぐ=否定する ￢(U3 ∧￢U1 ∧￢U2 ∧￢U3’) 15
- 16. アブダクションの必要性 ! ? 安全要求をFSRとして 機能モデル FSR ￢HZ01 ! ? からFSRを求めても FSR: HZ01 ￢HZ01 安全要求を出すつもり が安全目標に戻ってし ! ? 見たいなのしか出てこない まった ! ? これはハザードを防ぐと言っているだけ ! ? 間違いではないが、特に言う必要もない 16
- 17. ただし ! ? 内部構造などの情報を エンジン制御 U1 x1 システム U3 機能モデルに入れると x3 U2 x2 ! ? それに応じたテストケ U3’ ースや詳細化条件等を (U1∨U2)∧U3'?U3 得ることができる U1 U2 U3' U3 (U1 ∨U2)∧U3'?U3 HZ01 HZ02 T T T T T ? ? T T T T F T T F F F T ? ? T ! ? コンポーネントへの T T T F F T F T T T ? ? ? ? 詳細化安全要求を T F F T F T ? T T F F T F F F F T ? ? ? T 導出できる F T T T T ? ? F T F T F T ? F T T F F ? T F T F F T ? ? F F T T F T ? F F F T F T ? F F T F T ? ? F F F F T ? ? 17
- 18. 命題論理 ! ? AND, OR, NOT ! ? 色々な応用がある ! ? 「命題論理は役に立たない」とか言っても、実は裏で使 われている(特にFTA等)。本人が知らないだけ。 ! ? 抽象度の高い領域で有効 ! ? 網羅性をツールで確保できる ! ? 意味のあるトレーサビリティを確保できる ! ? 前ページの例ではアーキテクチャとテストケース ! ? ただし、 ! ? 注意しないと堂々巡りになる ! ? このままでは、振る舞いの記述は出来ない 18
- 19. 振る舞いの演绎 振る舞いは風、fluentは花 ! ? Fluentによって命題論理を拡張して振る舞い仕様 を生成することができる ! ? 贵濒耻别苍迟命题 ! ? 特定の動作で真偽が決まる命題 ! ? 振る舞い仕様 ! ? 状態マシンのこと ! ? つまり、贵濒耻别苍迟命题を使った論理式から状態マシ ンが出てくるということ 19
- 20. 振る舞いは風、fluentは花 その心は 神の影向を表す、榊の枝 からたれた垂のかすかな そよぎ そよぎ ≈ fluent 20
- 21. 要求と状態、振る舞いの例 ! ? 要求 走行中はドアを開けない ! ? 状態 ! ? 「走行中」と言う状態があることを示している この状態にMovingと名前を付ける ! ? 「ドアが閉まっている」と言う状態があることを示している この状態にClosedと名前を付ける ! ? 振る舞い ! ? 振る舞いによって状態が変わる 例: Startすると「走行中」 になりStopすると「走行中」ではなくなる 21
- 22. 贵濒耻别苍迟命题 ! ? 前ページのMovingやClosedを振る舞いに依存して真偽 が確定する命題と考える。これを贵濒耻别苍迟命题と呼ぶ。 ! ? Moving状態であることを示す論理変数と考える ! ? 贵濒耻别苍迟命题を使うと振る舞いに関する要求文を命題化 することが出来る ! ? 走行中はドアを開けない : Moving? Closed Moving Closed start stop time close open time Moving false true false Closed false true false 時間軸上での贵濒耻别苍迟命题の変化 22
- 23. (Moving?Closed)の意味 意味を理解するために、個別のコンポ ーネントの振る舞いからシステムで可 Car start 能な全ての状態を合成する 0 1 stop ! ? 車はスタート/ストップを繰り返す Door open Car = (start->stop->Car). 0 1 close ! ? ドアはオープン/クローズを繰り start Door = (open->close->Door). BM01 open start close 0 1 2 3 close stop open ! ? 車とドアの振る舞いを合成する stop 全状態空間 ||BM01 = (Car||Door). 23
- 24. ! ? 個々の状態に対して命題論理式を評価してみる start open start close BM01 0 1 2 3 close stop open stop Moving F F T T Closed T F F T 命題論理式 Moving Closed T T F T ! ? (Moving?Closed) は、この状態を禁止する安全要求 24
- 25. 状态を利用したモデリング ! Moving?Closed を満たす状態マシンを定義するのであ れば満たしていない状態を削除すれば良い start open open start close start BM01 BM01B 0 1 2 3 0 1 2 close stop open stop close stop Moving F F T T F T F Closed T F F T T T F Moving Closed T T F T T T T 25
- 26. 演繹を利用したモデリング ! ? 要求を時相論理式で表現する ! ? 時相論理式から状態マシンを生成する ?uent Moving = <{start},{stop}> initially 0 ?uent Closed = <{close},{open}> initially 1 assert AlwaysSafeDoor = [] (Moving->Closed) constraint LTL01 = AlwaysSafeDoor open start LT L01 0 1 2 {close, stop} {close, start} {open, stop} stop close 26
- 27. モデリングスタイル比較 ! アブダクション(状態ベース)によるモデリング ? ! 経験と勘によるモデリング ? ! 時間が掛かる上に正しいかどうか根拠が曖昧 ? ! ほとんどの場合、必要以上に複雑で間違いを含んだモデル ? になる ! ?別途検証が必須で開発工数が掛かる ! 演繹(時相論理式)によるモデリング ? ! 演繹に依るので無駄が無く正確 ? ! 自動生成で検証済みのモデルを得られる ? ! 結果として、シンプルで読みやすいモデルを得られる ? ! 実装?テストも簡単になる ? ! ただし、表現できない仕様もある ? 27
- 28. サンプル-1 ! ? 水位計の動作モデルを作成せよ ! ? 入力: 水位レベルは0..9まである ! ? level[0..9] この本に出てくる 演習問題 ! ? 出力: ! ? low " "水位レベルが2以下 ! ? high 水位レベルが9 ! ? normal LowでもHighでも無い時 28
- 29. サンプル-1 解答 ! ? 一般的なアブダクション解答 range Level = 0..9 SENSOR = SENSOR[5], SENSOR[w:Level] = (level[i:Level] -> SENSOR[i] | when (w<2) low -> SENSOR[w] | when (w>8) high -> SENSOR[w] | when (w>=2 && w<=8) normal -> SENSOR[w] ). level[0..1] level[9] level[0..1] AbductionSensor 0 1 2 {level[2..8], normal} {high, level[9]} {level[0..1], low} level[2..8] level[9] level[2..8] 29
- 30. サンプル-1 演繹解答 ! ? 演繹による解答 ?uent Low = <level[0..1],level[2..9]> initially 0 ?uent Norm = <level[2..8],{level[0..1],level[9]}> initially 1 ?uent High = <level[9], level[0..8]> initially 0 assert LowF = [](low -> Low) assert NormF = [](normal -> Norm) level[9] assert HighF = [](high -> High) level[0..1] level[9] DeductiveSensor constraint CLowF = LowF 0 1 2 constraint CNormF = NormF {level[2..8], normal} {level[0..1], low} {high, level[9]} constraint CHighF = HighF level[2..8] level[0..1] level[2..8] minimal ||DeductiveSensor = (CLowF||CNormF||CHighF) @{high, level[0..9], {low, normal}}. 30
- 31. 要求文à?论理式à?状态マシン ! ? 「low 水位レベルが2以下」 ! ? [](low -> Low) ! ? [](!Low -> !low) ! ? [](Low -> (low || level[0..1])) ちょっと設計っぽい ! ? 全て同じ状態マシンになる level[0..1] low アクション LOW 状態 CLowF 0 1 level[2..9] {level[0..1], low} Lowが真の状態 level[2..9] 31
- 32. モデル検査との比較 ! ? いわゆるモデル検査はアブダクションしたモデルを 検査式(assert文)で検証 ! ? 演繹モデリングは検査式を仕様としてモデルを生成 ! ? モデル検査は検査終了が分からない ! ? 何本検査式を通せば良いのか ! ? 同じ意味で形の違う検査式で検査するかも 32
- 33. サンプル-2 on/off scan reset ! ?FMラジオの動作モデルを以下のon, off, scan, reset, lock, endを使って作成せよ ! ? 入力 ! ? 電源スイッチ on, off ! ? チューナーボタン scan, reset reset : 受信周波数をトップ周波数にセットする scan : 周波数を下げながらFM局を探す ! ? 出力 ! ? lock : FM局に周波数をロック、scanを停止、再度scanボ タンを押されるとスキャンをおこなう ! ? end : 最低周波数に到達 33
- 34. サンプル-2 解答 ! ? 一般的なアブダクション解答 RADIO = OFF, OFF = (on -> TOP), TOP = (scan -> SCANNING | reset -> TOP | off -> OFF), SCANNING = (scan -> SCANNING | reset -> TOP | off -> OFF | lock -> TUNED | end -> BOTTOM), TUNED = (scan -> SCANNING | reset -> TOP | off -> OFF ), BOTTOM = (scan -> BOTTOM | reset -> TOP | off -> OFF). on scan end AbRADIO 0 1 reset 2 scan 3 scan off {lock, reset} off reset off 34
- 35. サンプル-2 演繹解答1 ! ? 演繹による解答 fluent OFF = <off, on> initially 0 fluent ON = <{on, reset, lock}, {off, scan}> initially 0 fluent SCAN = <scan, {end, lock, reset, off}> initially 0 fluent BOTTOM = <end, {reset, off}> initially 0 assert T1 = [](OFF -> X (ON && !BOTTOM && !SCAN )) assert T2 = [](ON -> X ((OFF || SCAN || reset) && !BOTTOM)) assert T3 = [](SCAN -> X (OFF || ON || BOTTOM || scan)) assert T4 = [](BOTTOM -> X ((ON || OFF || scan)&& ! SCAN)) assert INIT = (OFF && ! ON && !SCAN && !BOTTOM) constraint T1 = T1 constraint T2 = T2 constraint T3 = T3 constraint T4 = T4 constraint INIT = INIT ||DeRADIO = (T1||T2||T3||T4||INIT). 35
- 36. おっと、ぜんぜん违う on on off {lock, reset} scan end {lock, on} DeRADIO 0 1 2 3 {lock, reset} reset 4 scan 5 6 7 on {lock, reset} off reset off reset scan off reset off off on scan end AbRADIO 0 1 reset 2 scan 3 scan off {lock, reset} off reset off 36
- 37. オリジナルとの比较 ! ? 状態マシンを比較することで、解釈の違いや仕様 の読み取り漏れ等が明確になる ! ? 全然違うと見えたが4ヶ所のみ違う CheckDe off on scan end property ||PropDe = (DeRADIO). -1 0 1 2 reset 3 scan 4 ||CheckDe = (PropDe||AbRADIO). off {lock, reset} off reset AbにはあるがDeにない遷移 off scan property ||PropAb = (AbRADIO). CheckAb off on scan end ||CheckAb = (PropAb||DeRADIO). -1 0 1 2 3 4 DeにはあるがAbにない遷移 off reset {lock, reset} scan {lock, reset} off reset off on {lock, on} 37
- 38. 比較結果 1) Abではendしてからscan可能になっている。 scanの解釈の違い: Abはscanボタンの押下と解釈して いる。Deはscan機能の駆動と解釈している。 2) Deではoff状態でlock, reset可能になっている。 3) Deでは連続onが可能になっている。 4) Deではend後にlockが起こることを想定している。 38
- 39. DeRADIOを修正 ! ? On/offはスイッチの形状から、onを連続しておこなえない場合 off on scan end ! ? 動作制約を追加 DeRADIO2 0 1 2 reset 3 scan 4 ONOFF = (off->on->ONOFF). off {lock, reset} 同じ状態マシン off reset をget ! ? OFFでlock, resetはあり得ない off assert T1 = [](OFF -> X (ON2 && !BOTTOM && !SCAN && !lock && ! reset)) ! ? BOTTOMでlockはあり得ない assert T4 = [](BOTTOM -> X ((ON2 || OFF || scan )&& ! SCAN && !lock)) ! ? 最低周波数に局があったらどうなるのか、と考えると仕様モレ 39
- 40. 本当の演繹の話をしよう ! ? 演繹解答1は本当に演繹したのだろうか ! ? 状態マシンの単なる自動生成ではないだろうか ! ? 状態マシンの部分機構のアブダクション? ! ? 『要求分析によって満たすべき性質を抽出し、その性 質を持った状態マシンを生成する』であるべき ! ? 満たすべき性質一つ一つが要求項目 ! ? 要求項目と結果の関係が明確でないと何が正解 か分からない ! ? アブダクションと同じになったから何なのさ!! 40
- 41. 何が違うのか ! ? 演習解答1はアブダクション主体で作って、それを検証している だけの様に見える ! ? (自動生成としての)演繹手法を使っただけ 本質は何も変わって いない … 形式検証を超える 演繹開発… 自明なものを使った仕様のトップダウン構築 その組み合わせによる解釈の多様性への対応 … 41
- 42. 終わりのない何かを 終わるために あれもや りたい ! ? 理由を説明できるようにしよう もやりた い これ ! ? そのための要求分析だ!! あれも やりた い ! ? 要求分析と演繹を関連付けて 強力なものに変える これ も やり た い ! ? 要求分析こそ希望の光 これもや りたい 42
- 43. 要求分析しながら演繹で作る ! ? 手順 ! ? 振る舞いにより生成される状態を定義する ! ? 状態間の関係を定義する ! ? 包含関係 ! ? 排他関係 ! ? 順序関係 ! ? 関係から状態マシンを生成して合成する ! ? 状態や関係は自明なレベルまで分解して定義する ! ? 包含、排他、順序等の関係が要求項目となる 43
- 44. 状態定義 ! ? 要求文に記述されている状態をFluentで定義する ! ? どんな状態があるか、それは何で始まり、何で終わるの かを考える ! ? ?uent ON = <on, off> initially 0 ! ? ?uent SCAN = <scan, {lock, end, reset, off}> initially 0 ! ? ?uent TUNED = <lock, {reset, scan, off}> initially 0 ! ? ?uent RESET = <reset, {scan, off}> initially 0 44
- 45. 包含関係 ! ? ON状態の中にSACN, TUNED, RESET状態がある ! ? assert SP01 = []((SCAN || TUNED || RESET) -> ON) on SP01 0 {end, off} 1 {end, lock, on, reset, scan} off 設計領域の問題なのか要求領域の問題なのか on状態は複合状態と言うのは設計の発想? 45
- 46. 排他関係 ! ? TUNEDとRESET状態が排他的ならば ! ? assert SP02 = [] ! (TUNED && RESET) ! ? しかし、Top周波数に局があれば排他的にはな らないのでSP02は不要かも知れない reset SP02 0 {lock, off, scan} 1 reset {off, scan} 46
- 47. 順序関係 ! ? scan状態の後にlock状態になる ! ? assert SP03’ = [](SCAN -> X TURNED) ! ? これだと必ず局があることを期待している ! ? scanはend, offでも終了するから ! ? assert SP03 = [](SCAN -> X ( TRUEND || end || off)) SP03 scan 0 {end, lock, off, reset} 1 {end, lock, off, reset} 47
- 48. システム状態マシンの生成 ! ? 要求項目に対応する状態マシンを合成してシステム の振舞いを表す状態マシンを生成する ! ? この際、明確なトレーサビリティが定義される reset on scan reset DEFAULT SP01 0 {end, off} 1 {end, lock, on} 2 on 3 {end, on, reset} SP02 off {end, lock} scan off SP03 on off scan DEFAULT 0 {end, off} 1 {end, lock, on, reset} 2 on off {end, lock, reset} これが トレーサビリティ off 48 もしかしたらEND状態が必要かも
- 49. ! ? あれが出来る出来ないで 違いは何? はなく、もっと抽象度の高 いところで議論する必要 がある reset on scan reset DEFAULT 0 1 2 3 {end, off} off {end, lock, on} {end, lock} on scan {end, on, reset} ! ? 背景にある考え方(関係) off の違いは何か off on scan ! ? 背景が決まればいつ 何が出来るかは演繹 DEFAULT 0 {end, off} 1 {end, lock, on, reset} 2 on off {end, lock, reset} で確定する off ! ? 無理矢理作ればバグ on scan end になる AbRADIO 0 1 2 3 reset scan scan ! ? そこをはっきりさせないと off {lock, reset} off reset 砂地獄の子犬になる off 49
- 50. 演繹のメリット ! ? 本当の要求分析が可能になる ! ? どのような要求項目を追加するとどうなるのか 直ちに確認 ! ? 状態数や遷移数から正確な見積もりが可能 ! ? 要求項目の組み合わせによるシミュレーション ! ? 要求ベーステストの十分性確認が容易 ! ? 要求検証と仕様化を同時におこなえる 50
- 51. 时间の玩具 ! ? 時間制約の扱いは時間制約 の関係でまたいずれ ∫ (fluent)dt = len みたいな感じでduration calculus と繋がる 51
- 52. まずは、命题论理の桥を渡ろう 抽象解釈の森 公理的設計論寺 ガロア接続山 実は神護寺 カテゴリー神社 実は愛宕神社 理論と実践の往還を助けるツールたち 論理を楽しむ風流人たち 命題論理の橋 管理に浮かれる人々 箱と線の図と そのビジネスを楽しむ人々 かんぷうずびょうぶ ! ? 高雄観楓図屏風に学ぶこっちの世界とあっちの世界 ! ? まだ雲に被われたあっちの世界にあるものは? 52
- 53. ありがとうございました ! ? 参考書 ! ? 組み込みソフトへの数理的アプローチ ! ? 命題論理の使い方 ! ? 状態マシンの演繹生成 ! ? プログラム検証など ! ? 使用したツール ! ? LTSA - Labelled Transition System Analyser ! ? Concurrency: State Models & Java Programs ! ? Jeff Magee (著), Jeff Kramer (著) ! ? http://www.doc.ic.ac.uk/ltsa/ 53 Web上に公開されていたMaurits Cornelis Escher, およびFrancisco de Goya, 駒井哲郎, 狩野秀頼の作品、 石 川佳純の写真, 陽明文庫収蔵品の画像を勝手に使用しました、これらの作品等に敬意と感謝を示します。