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.