Structural Embedding: Mechanization with Method
Abstract
The most powerful tools for analysis of formal specifications are general purpose theorem provers and model checkers, but these tools provide scant methodological support. Conversely, those approaches that do provide a well developed method generally have less powerful automation. It is natural, therefore, to try to combine the better developed methods with the more powerful general purpose tools. An obstacle is that the methods and the tools often employ very different logics. We argue that methods are separable from their logics and are largely concerned with the structure and organization of specifications. We propose a technique called structural embedding that allows the structural elements of a method to be supported by a general purpose tool, while substituting the logic of the tool for that of the method. We have found this technique quite effective and we provide some examples of its application. We also suggest how general purpose systems could be restructured to support this activity better.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1999
- Accession Number
- ADA366800
Entities
People
- Cesar Munoz
- John Rushby