Developing a Decision Support Tool for Dam Management with SPIN

Motivation

Analysis of many critical systems is usually based on the simulation of numerical models. This solution is suitable for analyzing systems with continuous and deterministic behaviors that evolve over time. However, real critical systems are more complex and can exhibit non-deterministic behavior due to unexpected events. Furthermore, critical systems present both discrete and continuous behaviors, which interact regularly. Both features can be modeled with hybrid formal methods, taking advantage of exploration techniques like model checking.

We have selected dam management as a case study. A dam is a critical system that has a hybrid behavior, there are continuous variables such as the water level, and discrete states such as the opening degrees of the spillways. At present, Decision Support Systems, based on numerical models, are used to manage complete river basins. Dams are modelled as black boxes which store and release water. A Decision Support Tool (DST) for dam management provides information about the possible consequences of dam operator actions, which can help to ensure the safety of the dam, as well as the efficient use of the water. In this work we have used formal methods to model a dam as a hybrid system, and we have obtained decision support information from the analysis performed with model checking.

Partially supported by Befesa Agua and by grants P07-TIC3131 (Andalusia) and TIN2008-05932 (Spain).