A CCS/meje specification of a hydro-power plant

This report describes the formal specification of a case-study realized using the process algebra CCS/Meije. The reactive system specified is formed by an hydroelettric power plant and its software control system. This software drives some engines producing eletrical power, handles the bacin's sluices, checks the safe working of the plant and the water level in the bacin; moreover, it interacts with an operator, that solves by hand the critical situations in the plant's administration. The informal specification of the "overall system was provided by ENEL; the Italian elettric company; it was quite ambiguous and incomplete. Then, we have simplified it, retaining only those. aspects useful to show, the specification methodology that CCS/Meije permits, but avoiding, at the same time, to make trivial the case study. In next section we present the semplification, called User Requirement Specification (URS), of the original ENEL specification, obtained removing the (most of the) ambiguities. In section 3 we give a brief presentation of the syntax and informal semantics of the CCS/Meije process algebra [AB84]. Finally, in the last section we give the CCS/Meije formal specification of the URS.