|
Published Articles >> Table of Contents >> Abstract
IEEE Conference and Workshop on Engineering of Computer-Based Systems
p. 304
Using Automatable Proof Obligations for Component-Based Design Checking
Murali Rangarajan, University of Cincinnati
Perry Alexander, University of Cincinnati
Nael Abu-Ghazaleh, State University of New York at Binghamton
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ECBS.1999.755895
Send link to a friend
| Abstract |
|
The complexity of modern systems is reflected in a proportionate increase in the complexity of their design and verification. Formal analysis methods are of particular interest because they provide the mathematical foundation necessary for rigorous analysis; successful formal analysis of a system provides a high level of assurance of correctness and conformance with specifications. Unfortunately, for a number of reasons, formal analysis techniques have failed to scale to large systems. In traditional engineering disciplines, decomposition and component-based design activities have contributed substantially to effective design of large systems. Consequently, this paper presents some proof obligations that perform partial correctness checks on hierarchically designed systems. Since the obligations are applied locally, they avoid the state explosion associated with formal analysis of a large system. The obligations represent initial steps towards the goal of decompositional verification of designs.
|
 Additional Information
|
Index Terms- Design Checking, Compositional Analysis, Formal Verification, PVS
Citation:
Murali Rangarajan, Perry Alexander, Nael Abu-Ghazaleh,
"Using Automatable Proof Obligations for Component-Based Design Checking,"
ecbs,
p. 304,
IEEE Conference and Workshop on Engineering of Computer-Based Systems,
1999
|
|
