Towards the Compositional Verification of Real-Time UML Designs (bibtex)
Reference:
Holger Giese, Matthias Tichy, Sven Burmester, Wilhelm Schäfer, Stephan Flake, "Towards the Compositional Verification of Real-Time UML Designs", in 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, pp. 38–47, New York, NY, USA: ACM Press, September 2003.
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.
Links:
@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.}
}
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
Powered by bibtexbrowser