Proceedings of: 
The 21st International Conference on 
Computer Safety, Reliabiltiy and Security (SAFECOMP),
10-13 September 2002, Catania, Italy, LNCS, Springer-Verlag


Title:
Model-checking based on Fluid Petri Nets 
for the temperature control system of the ICARO co-generative plant



Authors:

Marco Gribaudo
Dip. di Informatica,
Universit\`a di Torino, 10149 Torino (Italy), 
email: marcog@di.unito.it

Andras Horv\'ath
Dept. of  Telecommunications,
Univ. of Technology and Economics, Budapest (Hungary)
email: horvath@webspn.hit.bme.hu

Andrea Bobbio
DISTA, Universit\`a del
Piemonte Orientale, 15100 Alessandria (Italy), 
email: bobbio@unipmn.it

Enrico Tronci
Dip. di Informatica, Universit\`a di Roma
"La Sapienza", 00198 Roma  (Italy), 
email: tronci@dsi.uniroma1.it

Ester Ciancamerla, Michele  Minichino
ENEA, CR Casaccia, 00060 Roma (Italy),
email: ciancamerla,minichino@casaccia.enea.it


Abstract

The modeling and analysis of hybrid systems is a recent and
challenging research area which is actually dominated by two main
lines: a functional analysis based on the description of the
system in terms of discrete state (hybrid) automata (whose goal is
to ascertain for conformity and reachability properties), and a
stochastic analysis (whose aim is to provide performance and
dependability measures). 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
(FPN). It is shown that the same FPN model can be fed to a
functional analyser for model checking as well as to a stochastic
analyser for performance evaluation. We illustrate our approach
and show its usefulness by applying it to a ``real world'' hybrid
system: the temperature control system of a co-generative plant.