Hybrid Techniques for Hybrid Systems

Computer controlled systems are almost omnipresent nowadays. We expect such systems to function properly at any time we need them. The malfunctioning of home electronics just irritates us, but glitches in a car, power plant or medical support system may threaten life, and faults in nuclear missile control facility may bring the end to civilisation. Such ubiquity of computer-based control puts very high reliability requirements on such systems. Hybrid systems combine continuous real-time behaviour and discrete events. Research in hybrid systems aims at providing means for reliable design and production of hybrid systems. In this thesis, we explore the world of hybrid systems. We acknowledge relevance and complexity of hybrid systems research, and emphasise several different research topics: modelling, analysis, testing and deployment of hybrid systems. We illustrate hybrid systems by presenting a collection of examples that reflect hybrid phenomena, its variety and occurrence in different applications. Of course, the list is not exhaustive, because only illustrative examples were chosen. However, it represents the diversity of hybrid systems sufficiently well to reveal the size and complexity of problems, and the broadness of the application area. We survey several major formalisms for modelling and analysis of hybrid systems. We overview an existing classification of hybrid systems, and propose a generalised classification scheme for diverse frameworks. Moreover, we classify the surveyed formalisms according to the proposed scheme. We propose a technique for stability estimation for a certain class of hybrid automata. It combines ideas from computer science and control theory, and is based on cycles detection and conservative gains estimation. We borrow the well-known algorithm for transforming a finite automaton into an equivalent regular expression for cycles detection from computer science. From control theory, we take the idea of conservative gains and use them to estimate stability of cycles. We introduce Behavioural Hybrid Process Calculus (BHPC), a formalism for modelling and analysis of hybrid systems. It combines process algebraic techniques and the behavioural approach [Polderman and Willems, 1998] to dynamical systems. We take an attempt to advance fusion of computer science and control theory in hybrid systems research. BHPC is based on two fundamental notions of actions and trajectories that describe discrete and continuous evolution of dynamical systems, respectively. At a higher abstraction level these two types of behaviour are treated uniformly, i.e., as normal elements of process algebra. Their behaviour is defined using structural operational semantics (SOS) rules [Plotkin, 1981, 2003]. Moreover, the rules already respect the differences between trajectory prefixes and action prefixes, based on our intuition on how such processes should behave. For example, in parallel composition trajectory prefixes are always required to synchronise, while for action prefixes interleaving semantics is adopted. Furthermore, we define a hybrid strong bisimulation relation for BHPC and prove that it is congruence. It is one of the most important properties to attain well-defined compositionality. Such a property allows interchanging bisimilar processes in any process algebraic expression. In other words, it allows refining process, changing their internal representation, and interchanging them without any losses as long as they manifest the same behaviour. We propose a technique for simulation of BHPC. We devise a simulation algorithm for a subset of BHPC operators and test some of the proposed techniques in the BHAVE prototype. The proposed simulation algorithm defines one of the possible ways to simulate Behavioural Hybrid Process Calculus. Moreover, we survey the major problems in simulation of hybrid systems in the light of BHPC and in a more general layout. For some of the issues we propose solutions, for the remaining we discuss potential ways to tackle the problems