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.
This work has been partially supported by the EUROFORM network and MURST funds.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
D. Austry, G. Boudol, Algèbre de processus et synchronisation, Theoretical Computers Science, 1(30), 1984.
J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill, Symbolic Model Checking for Sequential Circuit Verification, IEEE Trans. on Computer-Aided Design, Vol.13, N.4, pp. 401–424, Apr. 1994.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic Model Checking: 10 20 states and beyond, Information and Computation, 98, (1992).
R. Bryant, Graph-Based Algorithms for Boolan Function Manipulation, IEEE Trans. on Computers, Vol.C-35, N.8, Aug. 1986.
K.S. Brace, R.L. Rudell, R.E. Bryant, Efficient Implementation of a BDD Package, 27th ACM/IEEE Design Automation Conference, 1995.
E.M. Clarke, O. Grumberg, H. Haraishi, S. Jha, D.E. Long, K.L. McMillan, L.A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Formal Methods in System Design, Vol.6, N.2, pp. 217–232, Mar. 1995.
O. Cherkaoui, N. Rico, A. Bernardi, Specification and Analysis of a Security Management System, FME 94, LNCS 873, Springer-Verlag.
A. Dsouza, B. Bloom, Generating BDD Models for Process Algebra Terms, CAV 95, LNCS 939, Springer-Verlag.
R. Enders, T. Filkorn, D. Taubner, Generating BDDs for Symbolic Model Checking in CCS, Proceedings of CAV'91, Lecture Notes in Computer Science, 575, Springer-Verlag, 1991.
ENEL, Descrizione informale di un caso di studio tratto dalle specifiche funzionali di un automatismo coordinatore delle manovre degli impianti idroelettrici, Centro di Ricerca in Automatica, Rapporto Interno, Febbraio 1992.
S. Larosa, R. Pugliese, Using the specification language CCS/Meije for a case study: a Software Control System of a Hydroelectric Power Plant, Nota Interna B4–58, Istituto di Elaborazione delTInformazione-CNR, Pisa, 1994.
S. Minato, N. Ishiura, S. Yajima, Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation, 27th ACM/IEEE Design Automation Conference, 1995.
R. Pugliese, E. Tronci, Automatic Verification of a Hydroelectric Power Plant, Research Report SI/RR-95/15, 1995.
R. de Simone, D. Vergamini, Aboard Auto, Rapports Techniques 111, INRIA, Sophia Antipolis, 1989.
E. Tronci, Hardware Verification, Boolean Logic Programming, Boolean Functional Programming, Proceedings of LICS 95, IEEE Computer Society.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pugliese, R., Tronci, E. (1996). Automatic verification of a hydroelectric power plant. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_100
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_100
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive