The dissertation reports on research that enables the practical application
of model checking to an important class of software systems. Model
checking is a formal technique that determines whether or not a given property of a
system holds over all possible execution paths. The software system which was used
to motivate and to drive this research was a part of a NASA robot control
Model checking can be applied to any system with a finite space of reachable states. Properties are expressed in a temporal logic and the system is represented as a program in a finite state language. Model checking has been successfully applied to hardware systems which are generally finite state systems. Its application to software systems has been limited. Conventional representations of software systems typically have an intractably large or infinite state space.
The approach taken in this research is to apply model checking to an executable design-level specification of the software system. The executable design representation is an executable subset and dialect of UML and is called xUML. The design-level specification is tested through simulation and then critical properties are model checked. The executable design specification is then compiled to a conventional procedural language. The resulting software system should be more reliable and robust than a system which has only been validated by testing.
This dissertation defines and describes a design paradigm for developing representations of software systems (in xUML) to which model checking can be applied. This design paradigm yields software systems with structures similar to hardware systems. The xUML models have finite state spaces. The xUML systems are composed of components with the spatial modularity property which enables application of model checking of systems by model checking of individual components in a system context. Construction of systems from spatially modular components was found to enable model checking of substantially more realistic robot control systems.
The dissertation then defines and describes an abstraction algorithm which generates an abstract program which preserves the control flow properties of the concrete program. The abstraction reduces the number of traversals of selected loops in the program to a near-minimum number. Control flow properties can be modeled checked on the abstract program, which may have orders of magnitude smaller state spaces than the concrete program, with assurance that the same control flow properties hold on the concrete program as the abstract program. Application of the loop abstraction to the robot control system substantially increased the complexity of systems which could be model checked.
The third contribution reported in this dissertation integrates testing and model checking for software systems where the representation to be model checked is abstracted from the concrete program. This integration enables the detection of errors which may have been introduced into the model by a manual abstraction process. It also enables the location and identification of errors in the concrete system from the error trace of a failed model check of the abstract model.
The University of Texas at Austin, a thesis copy is available by
© 2002 Natasha Sharygina.