Italiano (Italian) English (Inglese)
Sunday, 23 June 2024

Technical Reports

Technical Report Details
Authors:Andrea Bobbio
Marco Gribaudo
András Horváth
Scientific Area:Formal Models
Title:From FPN to NuSMV: The temperature control system of the ICARO cogenerative plant
Published on:TR-INF-2002-02-02-UNIPMN
Publisher:Computer Science Department, UPO
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). The present technical report 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. The technical report describes the systems in terms of FPN, then shows how the FPN can be converted into a hybrid automata (following the specifications of the tool HyTech) and into a discrete model based on finite state machine according to the specifications of the tool NuSMV. The complete NuSMV specifications are finally provided, and some results derived using the tool NuSMV.