Affiliations: Institute of Informatics, Warsaw University, 02-097 Warsaw, Poland. {mengel,akret,jmd}@mimuw.edu.pl
Note: [] Address for correspondenece: Institute of Informatics, Warsaw University, 02-097 Warsaw, Poland
Abstract: The Trace Assertion Method (TAM) pioneered by Parnas is a formalism used to specify software module interfaces. The main purpose of the research described in this paper is to recognize the possibilities of linking the TAM editor with one of the existing theorem proving systems and to enable thereby the automated consistency checking of trace specifications. Possible approaches to embedding TAM in the Prototype Verification System (PVS) specification language are discussed and the chosen shallow definitional embedding is described in detail. Proof obligations for the consistency checking of trace specifications are obtained as type correctness conditions generated automatically by the PVS type checker. Some of these obligations can be proven automatically by PVS, other proofs need human guidance. Possible ways of increasing automation capabilities of the PVS theorem prover are recognized and presented. We share our experience in defining both specialized and general purpose proof strategies. This research may be viewed as a case study in applying the existing general purpose proof system to consistency checking of some application-specific formalism, which might be of interest for the software designer community.
Keywords: Software engineering, Formal methods, Automated theorem proving, Shallow and deep embedding, Axiomatic and definitional embedding, Trace Assertion Method, PVS
