OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Mutation of Formally Verified SysML Models

Apvrille, Ludovic and Sultan, Bastien and Hotescu, Oana Andreea and Saqui-Sannes, Pierre de and Coudert, Sophie Mutation of Formally Verified SysML Models. ( In Press: 2023) In: MODELSWARDS 2023 : 11th International Conference on Model-Based Software and Systems Engineering, 19 February 2023 - 21 February 2023 (Lisbon, Portugal).

[img] (Document in English)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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 contri- butions 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. In this latter case, our algorithm reuses as much as possible previous proofs results in order to lower the proof complexity. The paper focuses on reachability proofs, and relies on a real-time communication architecture based on TSN (Time Sensitive Network) to exemplify the approach and give performance results.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > Institut Mines-Télécom (FRANCE)
Other partners > Télécom Paris (FRANCE)
Laboratory name:
Deposited On:16 Dec 2022 15:16

Repository Staff Only: item control page