Current
verification technology has reached the maturity where it can be applied to
non-trivial embedded software applications. However, producing a correctness
proof for a system (the embedded software and its physical environnment) requires
building a model of the system and this is still an art. The software part of
a system can, in principle, be modeled automatically, but the physical part
of the system must be modeled manually and informally. If we then formally prove
a property of the model, we need a separate and essentally informal argument
that the system has this property too. Our trust in the correctness of the system
then partly depends on the quality of this essentially informal argument that
the model accurately represents the system. Our aim in this project is to find
techniques to enhance the quality of the model and of the informal argument
that it accurately represents the system.

Our approach is to use joint decomposition of the system model and the correctness
property, guided by the structure of the physical environment. The guidance
provided by the physical environment is given by engineering blueprints that
always exist of this environment, such as a P/I diagram. This decomposition
is non-monotonic, because the proof that the lower-level properties jointly
imply the composite correctness property may require the addition of axioms
that force us to change the proofs already given. We will facilitate this
process by identifying recurring patterns in the physical environment that
can be reused in correctness proofs.