Analysis and synthesis of reactive systems : a generic layered architecture perspective

Sammanfattning: This thesis studies methods and tools for the development of reactive real-time control systems.development framework is called Generic Layered Architecture (GLA). The work focuses 01analysis and synthesis of software residing in the lowest two layers of GLA, namely, the PnLayer and the Rule Layer. The Process Layer controls cyclic computation and the Rule Iproduces responses by reacting to discrete events. For both layers there exist earlier defined langisuitable for describing applications. The programs in the Process Layer and the Rule Layer are cPL and RL programs, respectively.Several issues are studied. First of all, we study the semantics and correctness of RL programs.includes providing semantics for desired responses and correctness criteria for RL programsintroducing operational semantics and static checkers together with some soundness results.combination of rules and reactive behavior, together with a formal analysis of this behavior, imain contribution of this work. The second issue is the estimation of the worst-case execution(WCET) of PL and RL programs. This work allows one to check if the computation resource osystem is adequate and aims at the predictability of GLA systems. It contributes to the realsystems area by performing WCET analysis on different execution models and language constfrom those studied in the literature. Finally, we deal with the synthesis of GLA software from alevel specification. More specifically, we motivate GLA as the framework to develop hcontrollers and present a semi-automatic tool to generate control software in GLA from a specificexpressed in terms of hybrid automata.These methods provide formal grounds for analysis and synthesis of software in GLA. Togetherthe language and tools developed previously, they ease the process of developing realcontrolsystems.