To improve the quality of software, formal methods are expected as a good solution, which enables rigorous analysis of the specifications of systems. We introduce the application of this technique to the specification of digital ATC Track database, in which the specification is analysed with automatic proof. In the specification, the invariants to be kept at any time as well as a small set of operations are defined. Proof obligations to verify the integrity of the specification are then generated automatically. All proof obligations are mechanically proved to the full although some proof obligations need help.

Copyright (c) 2002 Railway Technical Research Institute