NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Structural Embeddings: Mechanization with MethodThe 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 ID
19990064123
Acquisition Source
Langley Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Munoz, Cesar (Institute for Computer Applications in Science and Engineering Hampton, VA United States)
Rushby, John (SRI International Corp. Menlo Park, CA United States)
Date Acquired
September 6, 2013
Publication Date
July 1, 1999
Subject Category
Computer Programming And Software
Report/Patent Number
NAS 1.26:209360
ICASE-99-26
NASA/CR-1999-209360
Funding Number(s)
CONTRACT_GRANT: NSF CCR-95-09931
CONTRACT_GRANT: NAS1-97046
PROJECT: RTOP 505-90-52-01
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available