Publications
Details for GTBSF03_ag
| Title: Towards the Compositional Verification of Real-Time UML Designs |
| 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) |
| Written by: H. Giese, M. Tichy, S. Burmester, W. Schäfer, S. Flake: |
| in: September 2003 |
| Volume: Number: |
| on pages: 38-47 |
| Chapter: |
| Editor: |
| Publisher: ACM Press |
| Series: |
| Address: |
| Edition: |
| ISBN: 1-58113-743-5 |
| how published: |
| Organization: |
| School: |
| Institution: |
| ISSN: |
| Doi: http://doi.acm.org/10.1145/940071.940078 |
| File: ESEC03-GTBSF.pdf |
| URL: |
Note:
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.
Eintrag als Bibtex exportieren