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
system.
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
request .
© 2002 Natasha Sharygina.