Determining relevant model elements for the verification of UML/OCL specifications
Julia Seiter, Robert Wille, Mathias Soeken, Rolf Drechsler · 2013
Abstract—Modeling languages such as UML or SysML received signif-icant attention over the last years. They allow for an abstract description of systems already in the absence of a precise implementation or a hard-ware/software partitioning. Additionally considering textual constraints, for example provided by means of OCL, enables to automatically check the specified systems e.g. for consistency of the structure or reachability of certain system states. However, for the majority of verification tasks, not the entire model has to be considered. In this work, we propose an approach that automatically determines reduced system models, i.e. system descriptions that only include model elements which are relevant for the considered verification task. Con-sidering reduced models eases the access by the designer and supports incremental design and verification schemes. But most important, they improve the efficiency of the applied formal verification engine. Exper-iments demonstrate that already small reductions in the model lead to significant accelerations in the run-time of the verification engine.