In: Proceeding of the 16th International Conference on Application and Theory of Petri Nets, Turin, June 1995., pages 84-102. 1995.
Abstract: In this paper, we present how the specification of a case study, the Hydoelectric 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 well as possible, the technical details of the algebraic part of the specification.