Accession Number : ADA456814


Title :   A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs


Descriptive Note : Doctoral thesis


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : Chaki, Sagar J


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a456814.pdf


Report Date : 24 May 2005


Pagination or Media Count : 274


Abstract : This dissertation presents a framework for verifying concurrent message-passing C programs in an automated manner. First, programs are modeled as finite state machines whose states are labeled with data and whose transitions are labeled with events. The author refers to such state machines as labeled Kripke structures (LKSs). His state/event-based approach enables him to succinctly express and efficiently verify properties that involve simultaneously both the static (data-based) and the dynamic (reactive or event-based) aspects of any software system. Second, the framework supports a wide range of specification mechanisms and notions of conformance (i.e., complete system specifications can be expressed as LKSs and simulation conformance verified between such specifications and any C implementation). For partial specifications, the framework supports (in addition to LKSs) a state/event-based linear temporal logic capable of expressing complex safety as well as liveness properties. The framework enables one to check for deadlocks in concurrent message-passing programs. Third, for each notion of conformance, the author presents a completely automated and compositional verification procedure based on the counterexample guided abstraction refinement (CEGAR) paradigm. These verification procedures consist of an iterative application of model construction, model checking, counterexample validation, and model refinement steps. However, they are uniquely distinguished by their compositionality. In each of his conformance checking procedures, the algorithms for model construction, counterexample validation, and model refinement are applied component-wise. The statespace size of the models are controlled via a two-pronged strategy: (1) using two complementary abstraction techniques based on the static (predicate abstraction) and dynamic (action-guided abstraction) aspects of the program, and (2) minimizing the number of predicates required for predicate abstraction.


Descriptors :   *SOFTWARE ENGINEERING , *AUTOMATION , *SPECIFICATIONS , *MESSAGE PROCESSING , *C PROGRAMMING LANGUAGE , *COMPUTER PROGRAM VERIFICATION , ALGORITHMS , COMPOSITION(PROPERTY) , CLIENT SERVER SYSTEMS , CONFORMITY , ITERATIONS , LOGIC , COMPUTERIZED SIMULATION , COMPUTER PROGRAMMING , THESES , MAPPING


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE