Analysis of Hybrid Systems with NBac

Bertrand Jeannet

April 9, 2010

We give here some experimental results we obtained with the version of NBAC tool handling hybrid systems. We show that the dynamic partitioning technique implemented in NBAC is able to cope with complex discrete behaviour.

More precisely, we first give a framework for modelling a software controller programmed in the dataflow synchnonous language Lustre interacting with a physical environment defined by classical hybrid automata. LUSTRE is a domain-specific language for programming control-command systems that periodically sample imputs from their environment, computes outputs and moves to a new internal state. We refer to [3] for an overview of the synchronous paradigm. The framework includes the modelling of the sampling rate, the reaction time of the software controller, and a possible uncertainty in the occurence of communications.

We then illustrate the use of this framework with 2 case-studies:

The experiments were performed on a PC equipped with a 2 GHz Pentium M processor and 1GB of memory.