Incremental and Formal Verification of SysML Models
Vérification formelle et incrémentale de modèles SysML
Résumé
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 reacha-
bility 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.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|---|
| licence |
