Integration of model checking into software development processes
Abstract
Testing has been the dominant method for validation of software systems. As
software systems become complex, conventional testing methods have become inadequate.
Model checking is a powerful formal verification method. It supports
systematic exploration of all states or execution paths of the system being verified.
There are two major challenges in practical and scalable application of model checking
to software systems: (1) the applicability of model checking to software systems
and (2) the intrinsic complexity of model checking.
In this dissertation, we have developed a comprehensive approach to integration
of model checking into two emerging software development processes: ModelDriven
Development (MDD) and Component-Based Development (CBD), and a
combination of MDD and CBD. This approach addresses the two major challenges
under the following framework: (1) bridging applicability gaps through automatic
translation of software representations to directly model-checkable formal representations, (2) seamless integration of state space reduction algorithms in the translation
through static analysis, and (3) scaling model checking capability and achieving
state space reduction by systematically exploring compositional structures of
software systems. We have integrated model checking into MDD by applying mature
model checking techniques to industrial design-level software representations
through automatic translation of these representations to the input formal representations
of model checkers. We have developed a translation-based approach to
compositional reasoning of software systems, which simplifies the proof, implementation,
and application of compositional reasoning rules at the software system level by
reusing the proof and implementation of existing compositional reasoning rules for
directly model-checkable formal representations. We have developed an integrated
state space reduction framework which systematically conducts a top-down decomposition
of a large and complex software system into directly model-checkable components
by exploring domain-specific knowledge. We have designed, implemented,
and applied a bottom-up approach to model checking of component-based software
systems, which composes verified systems from verified components and integrates
model checking into CBD. We have further scaled model checking of componentbased
systems by exploring the synergy between MDD and CBD, i.e., specifying
components in executable design languages, and realizing the bottom-up approach
based on model checking of software designs through translation.