Determining relevant model elements for the verification of UML/OCL specifications

Julia Seiter, Robert Wille, Mathias Soeken, Rolf Drechsler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

Modeling languages such as UML or SysML received significant attention over the last years. They allow for an abstract description of systems already in the absence of a precise implementation or a hardware/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. Considering 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. Experiments demonstrate that already small reductions in the model lead to significant accelerations in the run-time of the verification engine.

Original languageEnglish
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE 2013
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1189-1192
Number of pages4
ISBN (Print)9783981537000
DOIs
StatePublished - 2013
Externally publishedYes
Event16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013 - Grenoble, France
Duration: 18 Mar 201322 Mar 2013

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
ISSN (Print)1530-1591

Conference

Conference16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013
Country/TerritoryFrance
CityGrenoble
Period18/03/1322/03/13

Fingerprint

Dive into the research topics of 'Determining relevant model elements for the verification of UML/OCL specifications'. Together they form a unique fingerprint.

Cite this