kirancodes.me
To Proof Maintenance & Beyond!
FSE 2003

Towards the compositional verification of real-time UML designs

Holger Giese, Matthias Tichy, Sven Burmester, Stephan Flake

PDFDOI 10.1145/940071.940078dblp

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.

BibTeX
@inproceedings{Giese-al:FSE03,
  author    = {Holger Giese and
               Matthias Tichy and
               Sven Burmester and
               Stephan Flake},
  title     = {Towards the compositional verification of real-time {UML} designs},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {38--47},
  publisher = {{ACM}},
  year      = {2003},
}

Related papers