TitleBasing a Modeling Environment on a General Purpose Theorem Prover
Publication TypeConference Paper
Year of Publication2004
AuthorsArcher, M.
Conference Name2004 Monterey Workshop on Software Engineering Tools: Compatibility and Integration
Conference LocationBaden, Austria

A general purpose theorem prover can be thought of as an extremely flexible modeling environment in which one can define and analyze almost any kind of model. A disadvantage to the full flexibility of a general purpose theorem prover is the lack of any guidance on how to construct a model and how then to apply the theorem prover to analyzing the model. In the general environment supplied by the prover, much time can be consumed in deciding how to specify a model and in interacting with and understanding feedback from the prover. However, specification templates, together with proof strategies whose design follows certain principles, can be used in many general purpose provers to create specialized modeling environments that address these difficulties. A specialized modeling environment created in this way can be further extended and/or further specialized in a straightforward way by drawing on the underlying theorem prover for additional capabilities. Moreover, a specialized modeling environment derived from a general purpose theorem prover provides a means of integrating powerful theorem proving capabilities into existing software development environments by way of appropriate translation schemes. This paper uses TAME (Timed Automata Modeling Environment) to illustrate the creation, extension, and specialization of a modeling environment based on PVS, and its integration into several software development environments.

Full Text


NRL Publication Release Number