|   | 
Author Pugliese, Rosario; Tronci, Enrico
Title Automatic Verification of a Hydroelectric Power Plant Type Conference Article
Year 1996 Publication Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3 Abbreviated Journal
Volume Issue Pages 425-444
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 μ-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.
Address (up)
Corporate Author Thesis
Publisher Springer Place of Publication Oxford, UK Editor Gaudel, M.-C.; Woodcock, J.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 1051 Series Issue Edition
ISSN 3-540-60973-3 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ fme96 Serial 53
Permanent link to this record