by Holger Giese
Abstract:
The trend towards more complex software within today's technical systems results in an increasing demand for dependable high quality software for real-time systems. In this report the foundations for the compositional pattern-based design of correct high level designs and architectures for real-time systems are presented. A formal calculus including a notion of discrete-time automata, a deadlock preserving refinement notion, and a class of supported compositional constraints is developed. It permits to design the required complex cooperation between the system components using verified patterns and includes support to derived the related correct component behavior in a systematic manner, such that the components itself do not invalidate the verified cooperation patterns.
Reference:
A Formal Calculus for the Compositional Pattern-Based Design of Correct Real-Time Systems. (Holger Giese), Technical report tr-ri-03-240, Lehrstuhl für Softwaretechnik, Universität Paderborn, 2003.
Bibtex Entry:
@TechReport{G03b_ag,
AUTHOR = {Giese, Holger},
TITLE = {{A Formal Calculus for the Compositional Pattern-Based Design of Correct Real-Time Systems.}},
YEAR = {2003},
MONTH = {July},
NUMBER = {tr-ri-03-240},
ADDRESS = {Paderborn, Deutschland},
INSTITUTION = {Lehrstuhl für Softwaretechnik, Universität Paderborn},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2003/tr-ri-03-240.pdf},
PDF = {tr-ri-03-240.pdf},
ABSTRACT = {The trend towards more complex software within today's technical systems results in an increasing demand for dependable high quality software for real-time systems. In this report the foundations for the compositional pattern-based design of correct high level designs and architectures for real-time systems are presented. A formal calculus including a notion of discrete-time automata, a deadlock preserving refinement notion, and a class of supported compositional constraints is developed. It permits to design the required complex cooperation between the system components using verified patterns and includes support to derived the related correct component behavior in a systematic manner, such that the components itself do not invalidate the verified cooperation patterns.}
}