Formal specification of cyber physical systems: Case studies based on hybrid relation calculus

Abstract

Hybrid system is a dynamic mixture of continuous physical world and discrete control part. In hybrid systems, continuous and discrete dynamic behaviors are displayed by the continuous and discrete components of the system respectively. Due to the complicated mixture mechanism, it becomes very difficult for us to model such a system accurately and explicitly. To simplify the modeling process, Jifeng He proposes a hybrid parallel programming language. It is in the light of his intellectual work that we can model physical world as well as its interaction with the control program. This paper aims to apply the programming language proposed by Jifeng He to the specification of hybrid systems. To describe this language specifically, we used a simple system which consists of a motor boat on a lake modeled by the space R2.This example illustrates that using hybrid relation calculus to specify hybrid systems can make every subsystem less complicated and more detailed, so that we can get easy access to observe the physical mechanism of the system.