ディジタルATCデータベースの証明による検証  [in Japanese] Analysis of Digital ATC Track Database Specification with Automatic Proofs  [in Japanese]

ディジタルATC線区データベース仕様を, コンピュータ上で行なわれる自動証明によって検証した.最初にデータベースの構造および最低限の操作に関する仕様を形式的仕様記述言語によって記述した.この仕様には軌道回路を始めとするデータベースの各構成要素間で常に満たさなければならない不変条件が記述されている.次にこの構造に矛盾のないこと, また操作によって不変条件が破壊されないことを保証するための証明責務を生成し, これを仕様とともに証明エンジンに投入した.一部の証明責務は自動で証明され, 残りの証明責務も証明エンジンを対話的に操作することにより証明された.すなわち仕様が矛盾のないことを完全に機械で証明することができた.

We analyzed the specification of the track database of Digital ATC with automatic proofs. The specification is written in a formal specification language, in which the invariants to be kept at any time and the minimum set of operations are specified. From the specification, proof obligations to ensure the integrity of the specification are generated. They are loaded into the proof engine and we tried to prove them. Some of the proof obligations are proved fully automatically and the others are proved interactively. Finally, we could prove all of the proof obligations fully mechanically.