Hybrid Interface Automata

Cyber-Physical Systems (CPS) are hybrid, component-based and open systems. Hybrid interface automata (HIA), which extend from interface automata, are introduced to model CPS. HIA are not input-enable, that is, only certain inputs can be accepted on a location of HIA. Thus, HIA can specify assumptions about the environment made by a component. HIA use an optimistic approach to composition, that is, two components are compatible if there is an environment in which they can work together. It is the important that HIA can describe the continuous behavior as well as the discrete behavior of a system. We give the algorithms for bounded checking the reach ability, well-formedness and compatibility of CPS. Technically, a bounded model checking on HIA is encoded as a dynamic programming. The algorithms for reach ability, well-formedness and compatibility checking are thus derived from genetic algorithms for solving dynamic programming. In comparison with the traditional algorithms in the theory of hybrid automata, which generally require that the model is linear, our algorithms relax the restriction.