@InProceedings{GTBSF03_ag,
AUTHOR = {Giese, Holger and Tichy, Matthias and Burmester, Sven and Sch\"{a}fer, Wilhelm and Flake, Stephan},
TITLE = {{Towards the Compositional Verification of Real-Time UML Designs}},
YEAR = {2003},
MONTH = {September},
BOOKTITLE = {Proc.~of the 9th european software engineering conference held jointly with 11th ACM SIGSOFT international symposium on foundations of software engineering (ESEC/FSE-11), Helsinki, Finland },
PAGES = {38--47},
ADDRESS = {New York, NY, USA},
PUBLISHER = {ACM Press},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2003/ESEC03-GTBSF.pdf},
PDF = {uploads/pdf/esec03-gtbsf.pdf},
ABSTRACT = {Current techniques for the verification of software as e.g.~model checking are limited when it comes to the verification of complex distributed embedded real-time systems. Our approach addresses this problem and in particular the state explosion problem for the software controlling mechatronic systems, as we provide a domain specific formal semantic definition for a subset of the UML 2.0 component model and an integrated sequence of design steps. These steps prescribe how to compose complex software systems from domain-specific patterns which model a particular part of the system behavior in a well-defined context. The correctness of these patterns can be verified individually because they have only simple communication behavior and have only a fixed number of participating roles. The composition of these patterns to describe the complete component behavior and the overall system behavior is prescribed by a rigorous syntactic definition which guarantees that the verification of component and system behavior can exploit the results of the verification of individual patterns.}
}