KAOS (90) 過程ベースの仕様 (4.4.2-2)

要求記述で,様相論理を使うこと場面は少ない.ただ,様相論理の発展形の一つである時相論理が使われるときがある.KAOSは,時相論理を用いる要求分析手法である.

時相論理という言葉は聞かなくても,モデル検証ということばは耳にするかもしれない.ミスリーディングと思うが,ここでのモデルとはふるまいのモデルのみを指す.時相論理は,設計者のものだけではなく,要求分析者が必要とする論理でもある.あるモデルが正しいか否かは,正しいとするプロパティが与えられて始めて確認できる.いくら立派な検証器があっても,プロパティが正しく設定できなければ,何も示していないことになる.アプリケーションに依存したプロパティは,要求定義をおこなう人のみが与えることができる.


 時間を気にせずにいえることは少ない.

例えば,「アクセル踏下するならば,踏下量に応じエンジン回転数を上げること」というのは,もちろんエンジンが動作している場合である.OFF状態で,いくら踏下しても,エンジン回転数は増加しない.

これは,単純に前提の問題だともいえる.前提に「エンジンが動作している」をAND結合すれば解決する.しかし,プリクラッシュが作動しているときはどうだろうか.

論理を拡張することによって,時間に関わる問題を解決するというのが,時相論理のねらいの一つである.私はX歳ですという言明は,X歳の時にしか真ではなく,その変化を論理として扱えるようにしようということである.

もともとは,並行プロセスや通信をどう扱うというところから主たる発展があった.ここでは,もう少し要求よりに次回から説明していく.

(nil)