Mutation of Formally Verified SysML Models

Mutation de modèles SysML formellement vérifiés

Ludovic Apvrille (1, 2) , Bastien Sultan (3, 4, 5) , Oana Hotescu (6, 7) , Pierre de Saqui-Sannes (6, 7) , Sophie Coudert (1, 2)

1 LabSoC - System on Chip
2 COMELEC - Département Communications & Electronique
3 LTCI - Laboratoire Traitement et Communication de l'Information
4 Télécom Paris
5 IP Paris - Institut Polytechnique de Paris
6 ISAE-SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace
7 UT - Université de Toulouse

Model checking of SysML models contributes to detect design errors and to check design decisions against user requirements. Yet, each time a model is modified, formal verification must be performed again, which makes model evolution costly and hampers the use of agile development methods. Based on former contributions on dependency graphs, the paper proposes to facilitate updates (also called mutations) on models: 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 paths that need to be re-verified. Our algorithm reuses the results of previous proofs as much as possible in order to lower the complexity of the proof. The paper focuses on reachability proofs. A real-time communication architecture based on TSN (Time Sensitive Networking) illustrates the approach and performance results are presented.

Keywords: Model Mutation; Model Checking; SysML; Time Sensitive Network

Domains: Modeling and Simulation

Ludovic Apvrille, Bastien Sultan, Oana Hotescu, Pierre de Saqui-Sannes, Sophie Coudert. Mutation of Formally Verified SysML Models. 11th internationl conference on Model-Based Software and Systems Engineering (Modelsward'2023), Feb 2023, Lisbonne, Portugal. ⟨hal-04002298⟩