Proceedings of:
Formal Methods Europe,
March 1996,  Oxford, UK,
Lecture Notes In Computer Science 1051, 
Springer

Authors:
R. Pugliese 
(Univ. di Roma "La Sapienza", pugliese@dsi.uniroma1.it)
E. Tronci 
(univ. di L'Aquila, tronci@univaq.it)



Abstract


We analyze the specification of a hydroelectric power plant by ENEL
(the Italian Electric Company). 
Our goal is to show that for the specification of the plant 
(its control system in particular) some given properties hold. 

We were provided with an informal specification of the plant. 
From such informal specification we wrote a formal specification
using the CCS/Meije process algebra formalism. 
We defined properties using mu-calculus.
Automatic verification was carried out using Model Checking. 
This was done by translating our process algebra definitions 
(the plant model) and mu-calculus formulas into BDDs. 

In this paper we present the informal specification of the plant, 
its formal specification, some of 
the properties we verified and experimental results.