Designing operational control architectures of critical systems by reachability analysis

This paper presents a method that eases the design of the operational architecture of a control system by providing, from the knowledge of some characteristics of the functions that the control system must ensure and a generic model of controller, an assignment solution of these functions that satisfies capabilities and distribution constraints. This method relies on the verification of a reachability property on a network of communicating automata that models the assignment process. The benefit of this proposal is illustrated by a non-trivial case study from industry.