Specification, abduction, and proof

Abstract

Researchers in formal methods have emphasized the need to make specification analysis as automatic as possible and to provide an array of tools in a uniform setting. Athena is a new interactive proof system that supports specification, structured natural deduction proofs, and trusted tactics. It places heavy emphasis on automation, seamlessly incorporating off-the-shelf state-of-the-art tools for model generation and automated theorem proving. We use a case study of railroad safety to illustrate several aspects of Athena. A formal specification of a rail-road system is given in Athena's multi-sorted first-order logic. Automatic model generation is used abductively to develop from scratch a policy for controlling the movement of trains on the tracks. The safety of the policy is proved automatically. Finally, a structured high-level proof of the policy's correctness is presented in Athena's natural deduction calculus. © Springer-Verlag 2004.