Pattern Synthesis from Multiple Scenarios for Parameterized Real-Timed UML Models (bibtex)
by , ,
Abstract:
The continuing trend towards more sophisticated technical applications results in an increasing demand for high quality software for complex, safety-critical systems. Designing and verifying the coordination between the components of such a system in order to ensure its overall correctness and safe operation are crucial and costly steps of the development process. In this paper, we extend our approach for the compositional formal verification of UML-RT models described by components and patterns [1], which addresses this challenge. We outline how scenario-based synthesis techniques can facilitate the design and verification steps by automatically deriving the required pattern behavior. Starting from a set of timed scenarios, the presented procedure generates a set of statecharts with additional real-time annotations that realize these scenarios. As parameterized timed scenarios are supported, different system configurations can be specified as required by adjusting the behavior using the specific timing constraints. The paper describes the proposed approach using a running example and presents first results obtained using a prototype implementation.
Reference:
Pattern Synthesis from Multiple Scenarios for Parameterized Real-Timed UML Models (Holger Giese, Florian Klein, Sven Burmester), Chapter in Scenarios: Models, Algorithms and Tools (Stefan Leue, Tarja Systä, eds.), Springer Verlag, volume 3466, 2005.
Bibtex Entry:
@InCollection{Giese+2005,
AUTHOR = {Giese, Holger and Klein, Florian and Burmester, Sven},
TITLE = {{Pattern Synthesis from Multiple Scenarios for Parameterized Real-Timed UML Models}},
YEAR = {2005},
MONTH = {April},
BOOKTITLE = {Scenarios: Models, Algorithms and Tools},
VOLUME = {3466},
PAGES = {193-211},
EDITOR = {Leue, Stefan and Systä, Tarja},
SERIES = {Lecture Notes in Computer Science (LNCS)},
PUBLISHER = {Springer Verlag},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2004/STTT-SMTT-BGK.pdf},
ABSTRACT = {The continuing trend towards more sophisticated technical applications
results in an increasing demand for high quality software for complex,
safety-critical systems. Designing and verifying the coordination between the
components of such a system in order to ensure its overall correctness and safe operation
are crucial and costly steps of the development process. In this paper, we
extend our approach for the compositional formal verification of UML-RT models
described by components and patterns [1], which addresses this challenge.
We outline how scenario-based synthesis techniques can facilitate the design and
verification steps by automatically deriving the required pattern behavior. Starting
from a set of timed scenarios, the presented procedure generates a set of
statecharts with additional real-time annotations that realize these scenarios. As
parameterized timed scenarios are supported, different system configurations can
be specified as required by adjusting the behavior using the specific timing constraints.
The paper describes the proposed approach using a running example and
presents first results obtained using a prototype implementation.}
}
Powered by bibtexbrowser