|
|
|
|
 |
|
|||||||||||||||||||
 |
Application name: ELSA (control system of a pondage power plant) Organisation: ENEL/CRA (research center of Automation of ENEL), the Italian Electric Energy Board, TXT Informatica, Politecnico di Milano. Method: TRIO (a temporal logic based language with metric on time) Tools: The TRIO tools environment was used, which includes: a graphical and textual (syntax-directed) editor; a history checker; and a test case generator. Domain: Miscellaneous Period: September 1994 - September 1995. Size: The formal specification document produced for the ELSA project included TRIO logical formulas and declarations of classes describing the system components, their relations and the system structure, and their graphical representation according to the syntax and semantics of the language. This document was about 120 pages long, including comments added to the logical formulas to increase readability. The total human effort involved in producing the specification was about 10 man months. Description: The project concerned the specification, validation, development and verification of the component of the control system of a pondage power plant that balances the load of electric power generation among the various generators according to strategies aiming at optimizing the use of the water available in the basin and at minimizing the wear of the generators. The system requirements were formally specified in TRIO and validated by means of simulation (history generation and checking). The specification was also used to generate test plans and its modular structure was employed to drive the design phase. Specification, test plans, and design+verification by testing were performed by distinc teams. Object-oriented principles and methods were extensively applied both during specification and design. Conclusions: Comparison of the outcomes of the ELSA project with similar applications developed by ENEL with more traditional develpment process indicate that the project was successful. The total amount of resources spent for developing the system was slightly decreased wrt similar applications, in presence of a significant change in the relevance of the various phases of the development: an increased effort in the initial specification and validation activities, supported by an extensive adoption of formal methods, facilitated all successive design, coding and acceptance phases, and reduced the overall costs. The quality of project documentation improved significantly, and the overall project was managed more easily. The introduction of the formal method did not cause organizational problems since the new development process easily fitted into the preceding one. The employed tools, still in a prototypal state, caused some problems (bugs, response time, etc.), which could however be overcome. Publications: M.Basso, E.Ciapessoni, E.Crivelli, D.Mandrioli, A.Morzenti, E.Ratto, P.San Pietro, "Experimenting a Logic-Based Approach to the Specification and Design of the Control System of a Pondage Power Plant", ICSE-17 Workshop on Industrial Application of Formal Methods, Seattle, WA, April 1995.
Contact:
|
|||||||||||||||||||
 |
||||||||||||||||||||
|
||||||||||||||||||||
© copyright 2004 | Formal Methods Europe |
||||||||||||||||||||
