Analysis and synthesis of reactive systems: a generic layered architecture perspective
1999 (English)Doctoral thesis, monograph (Other academic)
This thesis studies methods and tools for the development of reactive real-time control systems. The development framework is called Generic Layered Architecture (GLA). The work focuses on the analysis and synthesis of software residing in the lowest two layers of GLA, namely, the Process Layer and the Rule Layer. The Process Layer controls cyclic computation and the Rule Layer produces responses by reacting to discrete events. For both layers there exist earlier defined languages suitable for describing applications. The programs in the Process Layer and the Rule Layer are called PL and RL programs, respectively.
Several issues are studied. First of all, we study the semantics and correctness of RL programs. This includes providing semantics for desired responses and correctness criteria for RL programs and introducing operational semantics and static checkers together with some soundness results. The combination of rules and reactive behavior, together with a formal analysis of this behavior, is the main contribution of this work. The second issue is the estimation of the worst-case execution time (WCET) of PL and RL programs. This work allows one to check if the computation resource of the system is adequate and aims at the predictability of GLA systems. It contributes to the real-time systems area by performing WCET analysis on different execution models and language constructs from those studied in the literature. Finally, we deal with the synthesis of GLA software from a high-level specification. More specifically, we motivate GLA as the framework to develop hybrid controllers and present a semi-automatic tool to generate control software in GLA from a specification expressed in terms of hybrid automata.
These methods provide formal grounds for analysis and synthesis of software in GLA. Together with the language and tools developed previously, they ease the process of developing real-time control-systems.
Place, publisher, year, edition, pages
Linköping: Linköpings universitet , 1999. , 184 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 613
IdentifiersURN: urn:nbn:se:liu:diva-35717Local ID: 28268ISBN: 91-7219-630-0OAI: oai:DiVA.org:liu-35717DiVA: diva2:256565
2000-01-21, Estraden, Hus E, Linköpings universitet, Linköping, 13:15 (English)