Contract Based Program Models for Software Model Checking
Jesper Amilon, Dilian Gurov
TL;DR
This work addresses scalable model checking of C programs by using contract-verified components to build flow-graph abstractions that capture state-transformations while abstracting away intermediate states. It introduces flow graphs as a language-independent intermediate representation that can be automatically translated into $TLA^+$ (for TLC) and nuXmv models, enabling both explicit- and symbolic-model checking. Annotated programs and flow graphs are defined precisely, with a pushdown-system semantics that preserves program structure, including procedure calls and returns. The approach is demonstrated on an automotive Stee example, arguing for strong applicability to safety-critical embedded software and outlining future work on experimental evaluation, semantic preservation, and integration with summaries.
Abstract
Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of \emph{flow graphs}, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in~C.