A formal framework of reconfigurable control based on model checking
Hexuan Hu, Anne-Lise Gehin, Mireille Bayart · 2008
This paper proposes a formal framework for reconfigurable control, based on model checking. This framework first generates a flexible model (i.e., an execution structure) according to the diagnosis, then defines a temporal specification language to deal with the problems due to infinite execution cycles and non-determinism, and finally provides the algorithms that will automatically verify whether the updated model satisfies the desired specification.