Mutation of Formally Verified SysML Models

Abstract

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.