状態の意味

ソフトウェアの状態とは何か，単一のプログラムであれば全てのそこで定義されている変数を組合せることによって作られる1つ1つの組合せだろう．複数のプログラムが別々のスレッドまたはプロセスとして動いていればこれらの状態(ready, wait, run)等も考慮する必要がある．
これらの状態の1つ1つは，論理命題の真偽の組合せとして表現することができる．また全てを数え切ることもできる．即ち有限である．
ソフトウェアの仕様のレベルではその仕様が実数や整数を含んでいれば無限状態になるが，これらは実装の過程においてfloat , intなどの有限桁に落とされるので最終的には有限状態になる．モデル検査技術はこれらの状態を与えられたモデルに対して数え上げる．モデル検査技術を使ったプログラム検証ツール[1]はプログラムコードから状態を数え上げる．
UMLやSysMLの状態図の状態は人間が定義した恣意的なものである．論理命題の真偽とは関係なく思い付きで状態が定義され，後に矛盾が生じて修正される．恣意的に作ったとしても状態を対応する論理命題にマップしていくことで，足りない状態を補完することができる．また，個別の命題の真偽の組合せでは無く，ある論理式が真か偽かで状態を定義することもできる．階層化された状態図を描くこともあるが，上位の状態(合成状態)は論理式によって定義されるべきである．恣意的に作られた階層化状態図には必ず矛盾がありソフトウェアに落とせるようなものでは無い．

イベントとアクション

ソフトウェアの状態を構成しているもの(変数等)に許される基本操作(アクション)やこれらの変化を伴うイベントごとに1つの状態遷移が対応する．と考えることでソフトウェアをオートマトンとしてモデル化できる．
簡単なサンプルを考える[2]．3っのキーA, B, Cがあって，このキーをABAの順に押せばドアが開くとする．このソフトは以下の様にモデル化できる．

[2]のFig.1.3より

このモデルで，ドアが開いていると言う状態は状態4で成立する．

• pred₁: ドアが開いている

それは，初期状態1からABAのイベントシーケンスで到達するからである．状態と命題とのマッピングで言えば，状態4は「ドアが開いている」と言う命題が真であることに対応している．その他の状態はこの命題の偽に対応している．では，状態1, 2, 3を識別するのはどの様な命題だろうか．以下の様な命題を考える．

• P_A: Aが押された
  
• P_B: Bが押された
  
• P_C: Cが押された

P_Aは状態2と4で成立し，P_Bは状態3のみで成立する．P_Cのみが成立する状態はない．結局状態の意味は

• 状態1: 初期状態，P_B ∨ P_C
  
• 状態2: P_A
  
• 状態3: P_B
  
• 状態4: P_A ∧ pred₁

別の視点で，意味づけをすることも出来る．つまり別の命題を利用する．

• pred₂: 前の状態は2
  
• pred₃: 前の状態は3

pred₂は状態3のみで真となり、pred₃は状態4のみで真となる．またここ(状態4)でドアが開く結果となる．従って，ドアが開く場合最後に入力された順はA、B、Aの順であると結論付ることができる．この事から上で示した状態図が正しいこと，すなわち仕様を満たしていることが分かる．

形式的な話

ここの話を形式的に定義しておくと，状態図と一般に言っているものはオートマトン(Automaton)の一種と言えが，そのオートマトンは一般的に数学の本等では A = <Q, E, T, q₀>の様なタプルとして定義される．ここで，

• Q : 状態の集合
  
• E : 遷移ラベルの集合
  
• T ⊆ Q x E x Q : 遷移のセット
  
• q₀ : オートマトンの初期状態

である．言語理論などでは受理状態などを含める場合があるが，ソフトウェアの動作記述ではこれで十分である．ここまでで述べたことをこの定義に追加すると

• P : 命題の集合
• l : Q の要素と P の要素との対応を取るマッピング

を追加するということである．すなわち，A = <Q, E, T, q₀, P, l> となる．

まとめ

ソフトウェアの状態は，論理命題の真偽の組合せで定義できる．恣意的に描いた状態図であっても論理命題によって状態の意味づけをすることができる．この意味づけによって制御の正しさを証明することができる．モデル検査はこの様な検証を自動でやってくれる．
状態図をレビューする時も，論理命題による意味づけを利用することができる．漫然と図を眺めるのでは無く，解析的なアプローチが可能になる．解析した結果，論理命題がn個あれば，2ⁿ個の状態が生成されるので，この事を使って状態図が完全かどうか検証出来る．モデル検査ツールを使えば自動でやってくれるが，モデル検査用モデルも人間が書いている以上レビューが必要で，その様な時は論理命題による解釈が必要になる．

関連情報

1.CBMC
2.Systems and Software Verification: Model-Checking Techniques and Tools

Social Links