Premium
A practical use of model checking for synthesis: generating a dam controller for flood management
Author(s) -
Gallardo M. M.,
Merino P.,
Panizo L.,
Linares A.
Publication year - 2011
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.1048
Subject(s) - flood control , computer science , flood myth , controller (irrigation) , geography , archaeology , agronomy , biology
Program synthesis with automated methods has been an active research area for many years; however, we still lack well‐known and accepted techniques for this software engineering task. In this case, the design space to be considered is infinite, even when the solution is restricted to software that meets the requirements. In this paper we propose the use of model checking (MC) techniques to automatically synthesize controllers. Given a goal in the evolution of a plant, MC can be used to search for acceptable software controllers that enable the plant to evolve as desired. We also develop a realistic application in the context of a joint project with a major water reservoir management company. This application generates controllers for dam management during flood seasons. The controllers give the proper orders (open or close the outflow elements) at precise times in order to avoid disasters and to preserve the water level in the dam. Copyright © 2011 John Wiley & Sons, Ltd.