Towards automated consistency checking of module interface specifications

• Autorzy: Engel M. , Kret A. , Mincer-Daszkiewicz J.
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

software engineering; formal method; automated theorem proving; shallow and deep embedding; axiomatic and definitional embedding; Trace Assertion Method; PVS

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2000
• Tom: Vol. 42, nr 3,4
• Strony: 251--278
• Opis fizyczny: bibliogr. 25 poz.

Twórcy

autor

Engel M.

autor

Kret A.

autor

Mincer-Daszkiewicz J.

• Institute of Informatics Warsaw University ul. Banacha 2 02-097 Warsaw, Poland,