Hybrid Interface Automata for Component Interfaces

The modelling and verifying of hybrid systems attract more and more attentions recently. Hybrid automaton is widely used to model discrete and continuous behaviors of hybrid systems. In this paper, a hybrid interface automaton(HIA) is proposed based on hybrid automaton to model the interface behaviors of hybrid components. According to the interface type of components, we define two kinds of HIA to model interface behaviors respectively. The RHIA(Reactive HIA) is used to model the interface behavior of reactive component and AHIA(Active HIA) for active components. In addition, some composition operations for component interface models are given to facilitate component based software development. The main contribution is to describing a composable model of component interfaces with formal methods, which allows static compatibility checking for some kinds of components composition with their interface models. To illustrate the approach, a case study railroad gate control of CBTC is discussed.