Startseite > Publikationen > Publikationen


Giese, Holger;Flake, Stephan;Schäfer, Wilhelm;Tichy, Matthias;Burmester, Sven;Schilling, Daniela:

Towards the Compositional Verification of Real-Time UML Designs.

tr-ri-03-241, Jul. 2003


Current techniques for the verication of software as e.g. model checkingare limited when it comes to the verication of complex distributed embeddedreal-time systems. Our approach addresses this problem and in particularthe state explosion problem for the software controlling mechatronicsystems, as we provide a domain specic formal semantic denition for asubset of the UML 2.0 component model and an integrated sequence of designsteps. These steps prescribe how to compose complex software systemsfrom domain-specic patterns which model a particular part of the systembehavior in a well-dened context. The correctness of these patterns can beverified individually because they have only simple communication behaviorand have only a fixed number of participating roles. The composition ofthese patterns to describe the complete component behavior and the overallsystem behavior is prescribed by a rigorous syntactic definition which guaranteesthat the verification of component and system behavior can exploitthe results of the verification of individual patterns.




author = {Giese, Holger and Flake, Stephan and Sch{\"a}fer, Wilhelm and Tichy, Matthias and Burmester, Sven and Schilling, Daniela},
title = {Towards the Compositional Verification of Real-Time UML Designs},
number = {tr-ri-03-241},
institution = {University of Paderborn},
month = jul,
year = {2003},

BibTeX in die Zwischenablage kopieren