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.