要求を精緻化するために明示的・暗黙的に用いるドメインプロパティもまた間違っているかもしれない.(p.49)
例として挙げられているのは,LH 2904 便が,ワルシャワ空港で悪天候下着陸しようとして,滑走路上で正常に停止できなかった事故である(1993年).ここでの例は,M. Jackson の本 1からとしている.
ともに,事故そのものについては余り触れていないので,簡単に書いておく.
悪天候の中で,ワルシャワ空港に着陸しようとしていた航空機 A320-200 は,ウィンド・シア(急激な風速・風向きの変更)があるという情報から,規定に従いアプローチの速度を上げた.滑走路に降りたが,速度は速く横風のために,左脚を十分に接地しないままの滑走が続いた.また,停止のための各装置の作動が遅れた.その結果,滑走路をオーバーランしそうになり,障害物を避けるために右に曲がった.左翼が土手とぶつかり,燃料タンクが破損.火災が発生した.死者2名.負傷者68名.
事故調査報告書によると,ブレーキシステムは次の仕様になっていた.
1. グラウンドスポイラ
ONが選択され,次の「地上」条件に適合したときにスポイラが動作する
地上条件:両方の着陸装置のショックアブソーバが,共に6,300kg以上の加重を受けている.或いは,両方の着陸装置の車輪の回転速度が,共に72ノット(約時速133Km)を超えている.
2. 逆推力装置
ONが選択され,地上条件に適合した場合に動作する
3. 車輪制動
ONが選択され,地上条件に適合した場合に作動する
即ち,地上で停止するためには,全て「地上」条件を満足している必要があった.しかし,横風を受けて車輪は片側だけの接地であり,かつ滑走路がぬれていたため,スリップにより車輪回転からは正しい速度を計算できない状態であった.即ち,接地しているにも関わらず,地上にはいないとシステムは判断した.
Lamsweerdeさんの説明は,次になる 2
システム要求
ReverseThrustEnabled ↔ MovingOnRunway
(逆推力装置が可能なのは,滑走路上を移動しており,かつその時に限る)
ソフトウェア要求
reverse = ‘on’ ↔ WheelPulses = ‘on’
(リバース変数をon にセットならば,車輪の回転パルスがオンであり,かつそのときに限る)
仮定
WheelPulses = ‘on’ ↔ WheelsTurning
reverse = ‘on’ ↔ ReverseThrustEnabled
(車輪の回転パルスがオンならば,そのときに限り車輪は回っている)
(リバース変数をonに設定するのは,車輪が回っているときに限る)
ドメインプロパティ
MovingOnRunway ↔ WheelsTurning
(滑走路上を移動しているならば,車輪は回り,かつ車輪が回るのは,滑走路上を移動しているときに限る)
ソフトウェア要求に対して,仮定とドメインプロパティを組み合わせると,システム要求と同じとなることを,辿れると思う.
明らかに,ドメインプロパティが間違えていたということになる 3
(nil)