Verifying dynamic aspects of UML models

Mathias Soeken, Robert Wille, Rolf Drechsler

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

49 Scopus citations

Abstract

The Unified Modeling Language (UML) as a defacto standard for software development finds more and more application in the design of systems which also contain hardware components. Guaranteeing the correctness of a system specified in UML is thereby an important as well as challenging task. In recent years, first approaches for this purpose have been introduced. However, most of them focus only on the static view of a UML model. In this paper, an automatic approach is presented which checks verification tasks for dynamic aspects of a UML model. That is, given a UML model as well as an initial system state, the approach proves whether a sequence of operation calls exists so that a desired behavior is invoked. The underlying verification problem is encoded as an instance of the satisfiability problem and subsequently solved using a SAT Modulo Theory solver. An experimental evaluation confirms the applicability of the proposed approach.

Original languageEnglish
Title of host publicationProceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011
Pages1077-1082
Number of pages6
StatePublished - 2011
Externally publishedYes
Event14th Design, Automation and Test in Europe Conference and Exhibition, DATE 2011 - Grenoble, France
Duration: 14 Mar 201118 Mar 2011

Publication series

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

Conference

Conference14th Design, Automation and Test in Europe Conference and Exhibition, DATE 2011
Country/TerritoryFrance
CityGrenoble
Period14/03/1118/03/11

Fingerprint

Dive into the research topics of 'Verifying dynamic aspects of UML models'. Together they form a unique fingerprint.

Cite this