Fluid Petri Nets and hybrid model-checking: a comparative case study

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 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 (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.

Introduction

This paper investigates a unifying view between formal methods and stochastic methods for hybrid systems by proposing an analysis methodology based on Fluid Petri Nets (FPNs) [1], [16], [14]. The case study, that is used to illustrate the methodology, is a discrete state controller that operates according to the variation of suitable continuous quantities (temperature, heat consumption).

Model parameters are usually affected by uncertainty. A common way to account for parameter uncertainty is to assign to the parameters a range of variation (between a minimum and a maximum value), without any specification on the actual value in a specific realization (nondeterminism). Hybrid automata [3] and model checking tools [8] operate along this line. If a weight can be assigned to the parameter uncertainty through a probability distribution, the nondeterministic model is replaced by a stochastic model: the FPN formalism [16], [11] has been proposed to include stochastic specifications. Recently, probabilistic model checkers of Markovian models have also been implemented [4], [20].

This paper intends to show that a FPN model of a hybrid system can be used as an input model both for functional analysis as well as for stochastic analysis. In particular, this paper shows that the a FPN model can be translated into a hybrid automaton model [2], [24], a discrete model [5], or, finally, a discrete/probabilistic model [20].

FPN's are an extension of Petri nets able to model systems with the coexistence of discrete and continuous state variables [1], [16], [14]. The main characteristics of FPN is that the primitives (places, transitions and arcs) are partitioned in two groups: discrete primitives that handle discrete tokens (as in standard Petri nets) and continuous (or fluid) primitives that handle continuous quantities (referred to as fluid). Hence, in a single formalism, both discrete and continuous variables can be accommodated and their mutual interaction represented.

Even if Petri nets and model checking rely on very different conceptual and methodological bases (one coming from the world of performance analysis and the other from the world of formal methods), we attempt to gain cross fertilizations from the two areas. The main goal of this paper is to investigate the possibility of defining a methodology which allows us to apply a common FPN model both for formal specification and verification via model checking and for performance analysis.

We describe our approach and show its usefulness by using a meaningful ‘real world’ application. We take the control system for the temperature of the primary and secondary circuits of the heat exchange section of the ICARO co-generative plant [4] in operation at ENEA CR Casaccia as our example. The plant is composed of two sections: the gas turbine that produces electrical power and the heat exchange section that extracts heat from the turbine gases.

The comparative analysis documented in this paper using the case study, allows us to draw some preliminary conclusions about the modeling power of the tools and techniques we utilize and their analytical tractability.

The paper is organized as follow. Section 2 describes the case study. Section 3 introduces the main elements of the FPN formalism, provides a FPN model for the case study and show some results obtained with the simulator described in Ref. [10]. Section 4 introduces the concept of hybrid automata, provides the conversion of the FPN model into a hybrid automaton and analyzes the resulting hybrid automaton by means of the tool HyTech [18]. Section 5 shows how the same FPN model can be translated into a discrete model suitable for the model checker NuSMV [23] and provides some experimental results. Section 6 translates the FPN model into a DTMC model suitable for the probabilistic model checker PRISM [22]. Section 7 concludes the paper with some preliminary considerations about the modeling and analysis features of the different tools.