From control-command synchronous programs to hybrid automata

Hybrid automata are often cited as the best model to describe and analyze control-command systems. However, no formal link exists between this high-level description and the low-level implementation of the control law (in C for example). In this article, we propose a framework that computes from a synchronous program an equivalent hybrid automata. To do this, we use an intermediate model, namely sampled hybrid automata (or S-HA in short), that are a restriction of hybrid automata in which each location has a specific sampling rate. We show that these S-HA can be translated into equivalent hybrid automata, and show that we can automatically construct, from a control-command program, a S-HA. We also show that both models are equivalent w.r.t. the continuous trajectories.