Show simple item record

Compositional Verification by Model Checking for Counter-Examples

dc.contributor.authorTevfik Bultan ,en_US
dc.contributor.authorFischer, Jeffreyen_US
dc.contributor.authorGerber, Richarden_US
dc.description.abstractMany concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using "model checking". In this approach an abstract, finite-state model of the system is constructed; then an automatic check is made to ensure that the requirements are satisfied by the model. In practice, however, this method is limited by the "state space explosion problem". We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model -- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space. In this paper we present our compositional approach, and describe the software tools that support it. (Also cross-referenced as UMIACS-TR-95-98)en_US
dc.format.extent3954986 bytes
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3541en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-95-98en_US
dc.titleCompositional Verification by Model Checking for Counter-Examplesen_US
dc.typeTechnical Reporten_US
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtUMIACS Technical Reportsen_US

Files in this item


This item appears in the following Collection(s)

Show simple item record