Mutation of Formally Verified SysML Models - Laboratoire Traitement et Communication de l'Information Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Mutation of Formally Verified SysML Models

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

Résumé

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.
Fichier principal
Vignette du fichier
modelward2023.pdf (326.86 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
licence : CC BY - Paternité

Dates et versions

hal-04002298 , version 1 (23-02-2023)

Licence

Paternité

Identifiants

  • HAL Id : hal-04002298 , version 1

Citer

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⟩
104 Consultations
50 Téléchargements

Partager

Gmail Facebook X LinkedIn More