M. Gribaudo, A. Horváth, A. Bobbio, E. Tronci, E. Ciancamerla, M. Minichino
This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out.
Our approach is illustrated by means of a ``real world'' hybrid system: the temperature control system of a co-generative plant.