Enabling Incremental SysML Model Verification: Managing Variability and Complexity Through Tagging and Model Reduction

Designing complex software systems with model-based approaches encounters the recognized state space explosion problem. Typically, only a subset of models can be formally verified, forcing reliance on simulation or testing to verify the entire system. Furthermore, most formal verification tools require a complete reeval-uation of properties after even minor modifications to a model. Although incremental formal verification, particularly the incremental model-checking approach of TTool, has been proposed, it still requires modelers to manually select sub-models not facing state space explosion. Unfortunately, this manual model selection is susceptible to errors. This paper presents a twofold contribution to SysML models of software product lines. First, we introduce a SysML model tagging feature that enables designers to explicitly differentiate between various subsystems, such as core and optional features. Second, we develop and implement a model reduction algorithm using dependency graphs (DGs). This algorithm automatically deactivate model elements linked to specific tags, removing both the specified elements and all their logical dependencies provided the DG is acyclic. These two contributions are evaluated for their effectiveness in generating model variants. Together, they facilitate the creation of a core model and an associated set of models, each extended by additional model elements, and make it possible to rely on incremental model-checking. We have implemented the contributions in TTool and applied it to an integrated modular avionics system. This application enables to compare—both manual and automated—model reduction strategies and assess their benefits for TTool users.