A SOC-Based Formal Specification and Verification of Hybrid Systems

In order to specify hybrid systems in a SOC paradigm, we define Hybrid Doubly Labeled Transition Systems and the hybrid trace of it. Then we extend SRML notations with a set of differential equation-based expressions and hybrid programs and interpret the notations over Hybrid Doubly Labeled Transition Systems. By redefining the dynamic temporal logic dTL, we provide a logic basis for reasoning about the behavior of hybrid transition systems. We illustrate our approach by a case study about the control of a moving train, in which the movement of the train is regulated by ordinary differential equations.