Modular verification of a fault-tolerant active structure controller: an example

The decomposition of a system into modular components, together with abstractions of the components, can allow a computationally difficult global verification task to be broken into a number of smaller, more manageable verification subtasks. We provide the first known nontrivial application of modular verification in conjunction with the model-checking paradigm for verifying hybrid systems. We verify a fault-tolerant active structure control system. The control system is a version of one originally presented and analyzed by Elseaidy et al. (1994, 1997). While the minimization method of given by Elseaidy et al. is automated, it also requires the abstractions to have exactly the same behaviors as their implementations. Our verification methodology differs in that we must provide explicit abstractions of the system components. However, we allow abstractions that are more abstract than the components themselves. General guidelines are given for the development of suitable abstractions