TY  - CONF
AU  - Pugliese, Rosario
AU  - Tronci, Enrico
ED  - Gaudel, M.-C.
ED  - Woodcock, J.
PY  - 1996
DA  - 1996//
TI  - Automatic Verification of a Hydroelectric Power Plant
BT  - Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3
T3  - Lecture Notes in Computer Science
SP  - 425
EP  - 444
VL  - 1051
PB  - Springer
CY  - Oxford, UK
AB  - 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 μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-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.
SN  - 3-540-60973-3
UR  - https://doi.org/10.1007/3-540-60973-3_100
DO  - 10.1007/3-540-60973-3_100
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=53), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Pugliese+Tronci1996
ER  -