Dependency Graphs to Boost the Verification of SysML Models

Model-Based Systems Engineering has often been associated with the Systems Modeling Language. Several SysML tools offer formal verification capabilities, and therefore enable early detection of design errors in the life cycle of systems. Model-checking is a common formal verification approach used to assess the satisfiability of properties. Thus, a SysML model and a property can be injected into a model-checker returning a true/false result. A drawback of this approach is that the entire SysML model is used for the verification, even if the property targets a sub-system of the model. In this paper, it is suggested to rely on dependency graphs to avoid applying model checking to the entire system when only a subset of the latter needs to be taken into account. We formalize SysML models and properties, then we present new algorithms to generate and reduce dependency graphs, so as to perform verification on reduced models. A case study on Time-Sensitive Networking is used to demonstrate the efficiency and limits of this approach. The algorithms described in the paper are fully implemented by the free software TTool. Our method enables an improvement in run time between 3% and 90% depending on the state space to be traversed to verify the property.