２０１１年１１月１７日
状態遷移の種類と形式検証の使いどころ
アイシン・エィ・ダブリュ株式会社
技術本部 解析技術部
２０１１年１１月１７日
はじめに
•
背景
–
状態遷移を使えば、なんでも表現でき、形式検証によって
安全性が確認できるという誤った情報で、状態遷移に飛びつく
傾向があるが、正しい理解の下で状態遷移を使わなければ、
目指した効果は得られない。
–
安全な設計を行うには、元となる正しい知識が必要である。
安全の基本は、「教育」です。
•
発表の流れ
–
状態遷移図の使われ方の事例
–
状態遷移図の教育方法の説明
–
最後に、形式検証の有効な使いところの説明
２０１１年１１月１７日
自動販売機を例題にする
•
入力：お金：
50
円、
100
円、
•
入力：ボタン：
150
円ジュース購入ボタン、
200
円ジュー
ス購入ボタン
•
動作：お金を入れて、金額が満たされた状態で購入ボタ
ンを押すと、ジュースが購入できる。
２０１１年１１月１７日
自動販売機の状態遷移例
要求分析：まず、どの様な流れになるのかシナリオを作る。
•
ユースケースを検討
–
購入金額は、
50
円、
100
円を組み合わせとなる。
150
円のジュース購入例（
200
円投入
50
円おつり）
1. 50
円＋
50
円＋
50
円＋
50
円
⇒ ジュース購入
2. 50
円＋
50
円＋
100
円
⇒ ジュース購入
まずは、ユースケース１について
タイミングチャートを描いてみよう。
２０１１年１１月１７日
タイミングチャート例
50
円
100
円
150
円ジュース
200
円ジュース
総額
150
円ジュース
50
円
ジュース出力
おつり
一次入力信号
中間信号
出力信号
ユースケース１
２０１１年１１月１７日
お金の組み合わせは、非常に多いので、タイミング
チャートでは数が多くなりすぎる。
状態遷移図を使うことで、複数のユースケースをまとめ
て表現できる。
ミーリーマシンを用いた状態遷移図の例
[50円]
[50円]
[50円]
意味
合計50円
意味
合計100円
意味
合計150円
/ジュース1出力
意味
合計200円
[100円]
[ジュース1購入]
/ジュース1出力
返金50円
ユースケース１、ユースケース２を表現
ユースケース１
ユースケース２
[50円]
２０１１年１１月１７日
ミーリーマシンを用いた状態遷移図の例
[50円]
[50円]
[50円]
意味
合計50円
意味
合計100円
[ジュース1購入]
意味
合計150円
/ジュース1出力
意味
合計200円
[100円]
[ジュース1購入]
[ジュース2購入]
/ジュース1出力
返金50円
/ジュース2出力
[100円]
[100円]
200
円投入までの複数ユースケースを
表現したミーリーマシン
[50円]
２０１１年１１月１７日
シナリオ表現としての状態遷移図
•
ユースケースが多すぎるものは、状態遷移図を使うこと
で、複数のユースケースをまとめた「シナリオ」を表現で
きます。これによって、全体の振る舞いが解り、仕様を
明確にする事ができる。
•
注意点
–
ただしこのような状態遷移図は、そのままソフトウェア
として実装する事はできない。
–
もちろん形式手法によるチェックも意味がない。
•
理由は、この状態遷移図は、要求を理解するため描か
れた「シナリオ」だからです。
•
ここから、実装に必要な情報を抜き出す為の、「分析」
が必要である。
２０１１年１１月１７日
状態遷移図の分析観点：状態変数
•
状態変数には、下記の二つが混在していることに気を
つけるべきである。
–
状態（有限個）
–
記憶（無限個）
無限数：記憶
中身の量
(
××
ml)
中身の温度（℃）
発熱量（カロリー）
有限数：状態
空・満水
沸騰前・沸騰中・沸騰後
２０１１年１１月１７日
状態遷移図の表現：記憶の例
•
ミーリーチャートはフリップフロップ（論理演算）の振る舞い説明
の為に作られたが、あくまで振る舞いを説明するためのもので
あり、コード生成を意識した表現方法ではない。
保持
0
0
0
1
（ﾘｾｯﾄ）
0
1
0
1
0
（不定）
1
1
Q
R
S
出力
入力
(1,0)
(x,1)
Q1/0
Q2/1
ムーアーチャート
/0
(1,0)/1
(x,1)/0
Q1
Q2
ミーリーチャート
(x,1)/0
(0,0)/0
(0,0)/1
Q=(!R)&&(S||Q)
真理値表や、論理演算が正しいコード
振る舞いを説明する為に描く
変換
２０１１年１１月１７日
状態遷移図からコード生成
フリップフロップ回路の振る舞いを書いて、
最適化された論理演算が出力されるか？
コード生成する状態遷移図は、
状態と記憶を区別した物を対象とする。
Q=(!R)&&(S||Q)
(1,0)
(x,1)
Q1/0
Q2/1
ムーアーチャート
/0
(1,0)/1
(x,1)/0
Q1
Q2
ミーリーチャート
(x,1)/0
(0,0)/0
(0,0)/1
変換
最適化されたコードは自動生成されない
２０１１年１１月１７日
状態遷移図の整理例
–
状態（有限個）
–
記憶（無限個）
•
金額の組み合わせや、ジュースの種類は、有限個と考
えるかも知れない。
•
しかし、両方共に、数の設定を増減することができるの
で、無限と考えるべきである。
•
金額やジュースの種類は、「記憶」に分類される項目で
あり、状態として扱ってはいけない。
•
つまり、シナリオで用意した以外にも、お金の組み合わ
せや、ジュースの種類があると判断すべきである。
２０１１年１１月１７日
状態遷移図の分析観点：システム
•
お金の投入毎処理するのか？
「お金が投入された」は、不定期なイベント
連続投入された場合は、高速な応答性が要求される。
状態遷移図のような高度な制御を、高速起動させるべき
ではない。
•
対応方法
投入金額を高速計算する部分を外部に作る。
状態遷移は、定期的に外部へ総額を問い合わせるだけ
にする。
正しい状態遷移図は
正しい、システム設計の元で成立する。
２０１１年１１月１７日
AUTOSAR
ソフトウェアプラットフォームの概念
XX制御 コンポーネント XX制御 コンポーネント何をアプリケーションとして
何をシステム側とするのか
構造的な設計思想が必要。
高負荷・低速・定期的な処理
不定期あるいは、高速な処理
２０１１年１１月１７日
自動販売機の動作例
•
自動販売機の「状態」は、「動作の異なるポイント」として
考えると、
3
つに切り分けができる。
–
初期状態（待機）、お金のカウント（金額チェック）、ジュースの
取り出し（排出）。
待機
排出
金額のチェック
[50円]
[50円]
[50円]
意味
合計50円
意味
合計100円
[ジュース1購入]
意味
合計150円
/ジュース1出力
意味
合計200円
[100円]
[ジュース1購入]
[ジュース2購入]
/ジュース1出力
返金50円
/ジュース2出力
[100円]
[100円]
金額チェック
[50円]
２０１１年１１月１７日
タイマ成立
遷移条件２
初期状態
遷移先
お金の排出
条件動作
状
態
名
内部メモリを初期化
初期状態
排出終了
対象商品を点滅させる
ジュースの取り出し
ボタンが押される
金額が満たされる
対象商品を点滅させる
お金のカウント
コイン投入
遷移条件
1
ジ
ュ
ース
の
取
り出し
遷移先
条件動作
遷移条件１
ボタン
動作待ち
遷移先
条件動作
条件動作
遷移先
遷移条件
1
初期状態
表で整理して、状態遷移図へ
表を使って情報を整理し、状態遷移図へ変換する
状態遷移表は、
STM
だけではない。
仕様検討用の表はもっとシンプルな物を使うべき。
必要最低限の事を表に書き込み、整理する。
思考速度を落とさないシンプルさが重要。
検証用の表と、設計用の表は異なる。
初期状態
排出
[
コイン投入
]
[
ボタン
]
お金のカウント
[
タイマー
]
金額はこの中で
問い合わせ
２０１１年１１月１７日
状態遷移の書き方
•
状態遷移図は、シナリオ表現、仕様の表現とさまざまな
使い方があり、「状態」と「記憶」の区別が必要であるこ
とを説明した。
•
更に状態遷移図は記述方法についても、制限が必要で
ある。
•
状態遷移図は、自由度が高く、さまざま書き方ができる。
そのため、他者からの理解度が低く、理解するのに時
間が必要なケースがある。
•
しかし、書き方を限定することで、他者からの理解度を
上げる事ができる。
•
アイシン
AW
では、書き方を２種類に限定した。
２０１１年１１月１７日
状態遷移図の記述ルール制定について
•
アイシン・エィ・ダブリュでは、
1995
年から状態遷移表を
用いた制御開発を行ってきた。当時から拡張された
意味論を使用しており、現在の
Stateflow
と同等である。
（ムーアーをベースにハレルヤ以上の拡張がされていた）
–
状態の階層化、並列化が可能
–
イニシャライズと通常実行の区別
–
遷移条件と条件アクションが使用可能
–
自己遷移、インナートランジションが使用可能
–
タイマーによる強制遷移が標準ルール
残念ながら、自動生成ツールではない。⇒
Stateflow
へ
•
表⇒図：状態遷移図の描き方は、
15
年間の状態遷移に
関する設計的な考え方を継承している。
２０１１年１１月１７日
A
型：ウォーターフォール型状態遷移図
状態は上から下に流れるように、記述する。
下へ遷移する条件は
左側へ記述する。
遷移条件は真ん中より
上側へ記述する。
遷移線よりも左側に
記述したほうが
全体のバランスが良い。
状態の大きさには意味は持たせない。
状態の大きさが状態の優先度を示したり、
状態の重要度を示す事はない。
初期、中期、終了の３つに分けて図を描く
初期
中期は、初期遷移から流れる
系統で並列に並べて描く
終了
上へ遷移する条件は
右側へ記述する。
遷移条件は真ん中より
下側へ記述する。
遷移線よりも右側に記述したほうが
全体のバランスが良い。
リセット
制御は、不安定から安定へ⇒ウォータフォール同様、上流に戻すのはリスクがある
２０１１年１１月１７日
B
型：多状態・多遷移
hasChange(ST)
状態変数をチェック
状態変数と一致した
状態へ遷移する
function f1
function f2
function f3
function f4
function f5
{function f1}
{function f2}
{function f3}
{function f4}
{function f5}
[in(A)]
i[n(B)]
[in(C)]
[in(D)]
[in(E)]
A
B
C
D
E
[ST==A]
[ST
==
B]
[ST
==
C]
[ST
==
D]
[ST
==
E]
２．遷移条件が多い場合は、
パラレルチャート化し、外へ出す。
１．インナートランジションを活用し
遷移線をまとめる。
２０１１年１１月１７日
A,B
混在型：状態遷移図の描き方
•
状態遷移図は、
A
型ウォーターフォール型を基本に
多遷移の
B
型を組み合わせ事で全ての表現が可能。
状態遷移は適切な記述を行えば、爆発しない。
２０１１年１１月１７日
具体的な事例説明
拡張階層構造化状態遷移表設計手法
Ver2.0
状態遷移表から状態遷移図へ変換する
参考資料
P54
から
２０１１年１１月１７日
B
型を使った状態遷移表現
MainS 2 S0 S1 ON S2 S3 S4 S5 S6 S7 S8 S9 subCartMainS 1 function fcn_ S2 function f cn_ S3 function f cn_ S4 function f cn_ S5 function f cn_ S6 function f cn_ S7 function f cn_ S8 [Button==E1] [Button==E0] [Button==E2] [Button==E3] [Button==E4] 1[hasChanged ( enum_ MainS) ]
2 1[enum_MainS==S3] 2 [enum_MainS==S4] 1 2 [enum_MainS==S5] 1 2 [enum_MainS==S6] 1 2 [enum_MainS==S7] 1 2 [enum_MainS==S8] 2 1 [enum_MainS==S9] [in( MainS.S2)] {fcn_ S2( ) ;} 1 2 [in(MainS.S3)] {f cn_ S3() ;} 1 2 [in(MainS.S4)] {f cn_ S4() ;} 1 2 [in(MainS.S5)] {f cn_ S5() ;} 1 2 [in(MainS.S6)] {f cn_ S6() ;} 1 2 [in(MainS.S7)] {f cn_ S7() ;} 1 2 [in(MainS.S8)] {f cn_ S8() ;} 1 2
