An incremental specification of a hydroelectric power plant control system using a class of modular algebraic nets

In this paper, we present how the specification of a case study, the "Hydroelectric Power Plant Control System", proposed by the ENEL S.p.A., the major italian electricity supplier, can be incrementally obtained using OBJSA nets, a class of modular algebraic high-level nets, supported by their environment ONE. OBJSA nets, which result from the integration of Superposed Automata (SA) nets and of the algebraic specification language OBJ, stress the possibility of building the system model through composition of its (sequential non-deterministic) components and encourage the incremental development of the specification and its reusability, thanks to the availability of the Redp and Redt transformations. The environment ONE supports the user in producing and executing a specification, hiding from her/him, as much as possible, the technical details of the algebraic part of the specification.