Incremental and Formal Verification of SysML Models

Agile methods are now commonly used to design critical systems. They consist in progressively doing increments to a model, and subsequently checking that all previously checked properties are still satisfied. Yet, model-checking is not inherently incremental, which means that all proofs must be redone at each stage, where one would expect to redo proofs only for parts of the systems that have been impacted by the modification. This makes model evolution costly and hampers the use of agile development methods. The paper proposes to facilitate model updates (also called mutations): whenever a mutation is performed on a model, the algorithms introduced in this paper can determine which proofs remain valid and which ones must be performed again. The main idea to reduce the proof obligation is to identify new possible execution paths that need to be re-verified. Our algorithm reuses the results of proofs applied to a previous model version. The paper applies this approach on dependency graphs generated from SysML models: our generic propagation algorithm can rework mutated dependency graphs so as to deduce more simple properties to be proved on reduced dependency graphs. Our approach can handle reachability properties and discusses extensions to liveness properties. The embedded system of an autonomous vehicle, characterized by real-time communication constraints, exemplifies the challenges and relevance of our approach.