Abstract
Original language  English 

Awarding Institution 

Supervisors/Advisors 

Thesis sponsors  
Award date  6 Sep 2006 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9036523974 
Publication status  Published  6 Sep 2006 
Fingerprint
Keywords
 METIS239016
 EWI9609
 FMTFMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
 IR57124
Cite this
}
Hybrid Techniques for Hybrid Systems. / Krilavicius, T.
Enschede : Centre for Telematics and Information Technology (CTIT), 2006. 192 p.Research output: Thesis › PhD Thesis  Research UT, graduation UT › Academic
TY  THES
T1  Hybrid Techniques for Hybrid Systems
AU  Krilavicius, T.
PY  2006/9/6
Y1  2006/9/6
N2  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 computerbased control puts very high reliability requirements on such systems. Hybrid systems combine continuous realtime 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 wellknown 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 welldefined 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.
AB  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 computerbased control puts very high reliability requirements on such systems. Hybrid systems combine continuous realtime 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 wellknown 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 welldefined 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.
KW  METIS239016
KW  EWI9609
KW  FMTFMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
KW  IR57124
M3  PhD Thesis  Research UT, graduation UT
SN  9036523974
PB  Centre for Telematics and Information Technology (CTIT)
CY  Enschede
ER 