KAOS (109) イベントベースの仕様 (4.4.4-3)

前回は,モード遷移表について見た.観測変数に対して,このモード遷移表を作成するためであった.次の2つのテーブルは,制御変数の状態を定めるために用いる.

イベント表(Event Table)

イベント表は,モードとイベントの関係を示す.

モードには様々な視点がある.下表における停車中(Stopped)・移動中(MovingOK)・高速走行中(TooFast)モードは,速度を観測変数とし,列車の移動に着目したときの様々なモードである.これらをまとめて,AMC(Associated Mode Class)と呼ぶ.ここでは,移動に着目するので,「移動状態(MovementState)」という名前を与える.

一方で,何かトラブルが,この移動状態AMCにおいて生じた時,別の視点から整理が必要である.下表における緊急(Emergency)が相当する.下表は,この別視点である「緊急」と移動に着目したAMCとの関係を示したものと考える.

イベント表

イベント表

制御変数の様々な値と,モードとイベントの関数としての項(Term)と呼ぶ.例えば,先の緊急は一つの「項」である.移動状態AMCにおいてAlarmが,ONのとき,Emergencyは,真になり,AlarmがONで,Reset=Onのトリガーが入った時に,Emergencyは偽となる.項というのは,モードをまとめて別名をつけたものとなる.一度,項として定義すれば,以降で,Emergencyを扱いやすくなる.

条件表(Condition Table)

条件テーブルは,AMCモードや状態の関数として,制御変数や項の種々の値を定義したものである.状態は,観測変数・制御変数・内部変数を用いて,述語として定義する.

下記に例を示す.

条件テーブル(Condition Table)

条件テーブル

ここで注目するのは,ドア状態(DoorsState)である.これもまた別の視点である.ドア状態は,ここまでに見た観測変数の状態,停車中等の状態を用いて,定めることができる.プラットフォームに入っているか,緊急状態であるとき,停車中モードである.かつ,動いていない(MovingOK, TooFastではない)時に,ドアは開く(Open)ことができる.

(nil)

KAOS (108) イベントベースの仕様 (4.4.4-2)

SCR

SCRは表を中心的な表現手段として用いる.以下の表を用いる.

  • モード遷移表(観測変数)
  • イベント表(制御変数)
  • 条件表(制御変数)

括弧内は,観測変数/制御変数のうち,どちらに対するものかを示している.観測変数は,環境中で関心のある情報であり,環境から機械(システム)に伝わる.制御変数は,システムが環境に働きかけるときの情報である.

モード遷移表

最初のモード遷移表について見てみる.以下が,境界書で用いている列車の例である.

mode_transition_table

モード遷移表(MovementState モードクラス)

モード遷移は状態遷移と考えることができる.モードが状態に相当する.表題にあるモードクラスとは,観測変数に関する状態遷移を示している.ここでの観測変数とは,列車の速度であり,上記で measuredSpeedとして示される.

一行目を見てみる.自車速度がゼロであれば,車両は停止状態となる(新しいモードStopped).この表で違和感を感じるかもしれない.制御変数ではなく,観測変数に対する遷移表であることを思い起こす必要がある.

@Tの定義を見てみる.

@T(P1) WHEN P2

この意味は,「P2が真であるとき,P1はあるタイミングで,偽から真に変わる」である.即ち,P2 ∧ ¬P1∧P1’ である(ここでプライムは,Z言語で見たように,イベント受信後を指す).

@T(measuredSpeed = 0) イベントの場合だと,観測変数である列車速度について,次の説明となる.括弧内の否定(列車の速度が0ではない)ときは,MovingOKという古いモードである.括弧内が成立したとき(0になった瞬間),Stoppedにモードが変化する.

(nil)

KAOS (107) イベントベースの仕様 (4.4.4-1)

Aiming at a very high quality documentation which has these properties is perhaps the only way out available today to deal with the problems encountered in the design of ultra-reliable software.

実務的には,こういった特性を持つ高い品質の文書を目指すことこそが,超ー信頼可能なソフトウェアの設計において,我々が出会うであろう問題を扱うために唯一可能なことである(SCR論文中から)

イベントベースとは

ここでは,組み込みシステムに典型的に見ることのできる,状態遷移で表現することが適切なシステムの記述法である.基本的な要素は,イベントとイベントを受け入れる状態および受け入れ後の遷移によって記述する.幾つか注意が必要である.ここでの状態は,前回までの「状態ベース」という時の状態とは直接には関係がない.もちろん,本には,「書架にある」・「貸出中である」という状態が存在し,貸出イベントによって,「書架にある」から「貸出中である」に遷移すると考えることもできる.しかし,状態ベースというコトバが指し示すのは,一般に(公理的)集合論に基づく表現に対して与えられる.ある作成する対象(システムであったり,その構成品)のふるまいを規定する状態とは異なっている 1

イベントベースの記述には,SCR, RSML, STATEMATE, LTS, ペトリネットなどがあるが,ここでは,SCR(Software Cost Reduction) 2を取りあげている.

SCRは,一般的なコントローループラントモデルに基づく文書化の方法を示したものである.4つの要素を持つ;機械(システム),環境,観測変数(環境から機械に情報を伝えるため),制御変数(機械から環境に働きかけるため).

次回から,しばらく,SCRについて見ていくこととする.

(nil)

Notes:

  1. 専門用語というだけである.例えば,モデル検査というときのモデルも有限状態機械モデルを短くモデルと呼んでいるだけであり,そこには静的モデルは含まれないことと同様である
  2. P. J. Courtois and D. L. Parnas, “Documentation for safety critical software,” Software Engineering, 1993. Proceedings., 15th International Conference on, Baltimore, MD, 1993, pp. 315-323.