We consider a simple machine running two different processes. Starting and finishing a process is indicated by the events a1, a2 and A1, A2 respectively. The events ah and Ah report starting and successful completion respectively to a superordinated operator.
Nominal Controller Design
The nominal plant behaviour and the nominal specification are shown below. During nominal operation the controller has to announce the starting and completion of a process to the operator before another process is allowed to start. Observe that the specification defines the semantics of the high-level events.
A controller that ensures the minimally-restrictive non-conflicting, complete and controllable closed-loop behaviour is shown below.
Fault-Accommodating Controller DesignThe occurrence of a fault manifests itself in the breakdown of the recently started process. This is indicated by the completion of the complementary process. The fault-accommodating plant model is set up from the nominal plant behaviour and the plant-failure behaviour.
The fault-accommodating plant behaviour is given by the union of the nominal plant behaviour and the plant-failure behaviour. Observe, that in this example the fault-accommodating plant behaviour equals the plant-failure behaviour.
Once a process fails, a fault-accommodating controller may still start the remaining process before reporting back to the operator. Thereby, the controlled system remains operational, while preserving the semantics of the high-level events. A respective specification and the resulting controller are shown below.
In order to compute a reconfigurator that ensures for an arbitrary nominal controller a non-conflicting, complete and controllable closed-loop behaviour while satisfying the specification requirements, we set up the formal plant Lf||Hv↑ form the virtualised nominal controller Hv and the fault-accommodating plant behaviour Lf, both shown below.
We define the high-level semantics according to the fault-accommodating specification from the above section and, additionally, we demand the 1-by-1 passing of events during nominal operation, i. e. we add the inactivity conditions shown below to the design specification.
The resulting reconfigurator is pictured below.
Remember that the occurrence of a fault in process 1 is indicated by the occurrence of the event A2 while A1 is expected and vice versa for process 2. Thus, a fault occurs in states S4 or S5. Observe that events are passed by 1-by-1 before the occurrence of a fault and afterwards the logical order of virtual events is consistent with the virtualised controller, while the physical events match the fault-accommodating specification.
In order to validate that the reconfigurator indeed ensures admissible closed-loop behaviour for any nominal controller, observe that there are exactly two distinguishable, non-minimally restrictive but complete solutions to the nominal control problem.
The respective closed-loop system are shown below
Obviously both closed-loop system fulfil the critical liveness properties completeness and non-conflictingness