Publications
Details for BGHS04_ag
| Title: Incremental Design and Formal Verification with UML/RT in the FUJABA Real-Time Tool Suite |
| Booktitle: Proc. of the International Workshop on Specification and Validation of UML Models for Real Time and Embedded Systems, SVERTS2004, Satellite Event of the 7th International Conference on the Unified Modeling Language, UML2004 |
| Written by: S. Burmester, H. Giese, M. Hirsch, D. Schilling: |
| in: October 2004 |
| Volume: Number: |
| on pages: 1-20 |
| Chapter: |
| Editor: |
| Publisher: |
| Series: |
| Address: |
| Edition: |
| ISBN: |
| how published: |
| Organization: |
| School: |
| Institution: |
| ISSN: |
| Doi: |
| File: SVERTS04.pdf |
| URL: |
Note:
Abstract: Model checking of complex time extended UML (UML/RT) models is limited today due to two main obstacles: (1) The state explosion problem restricts the size of the UML/RT models which can be addressed and (2) standard model checking approaches cannot be smoothly integrated into the usually incremental and iterative design process. The presented solution for incremental design and verification with UML/RT within the FUJABA Real-Time Tool Suite overcomes these two obstacles by applying a compositional reasoning approach [1] that is based on a restricted notion of UML patterns and components. A mapping of a subset of the UML/RT component model and additional real-time extensions for UML state diagrams to HUppaal enables the automatic, compositional formal verification of partial models such as patterns and components by means of a model checking Plugin [2]. This tool support makes an incremental and iterative design and verification process possible where only the patterns and components which have been modified have to be rechecked rather than the whole UML/RT model.
Eintrag als Bibtex exportieren