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.