A Simple-Machine Example

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.

Nominal Plant Nominal Specification

A controller that ensures the minimally-restrictive non-conflicting, complete and controllable closed-loop behaviour is shown below.

Nominal Controller

Fault-Accommodating Controller Design

The 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.
Nominal Plant 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.

fault-accommodating specification Fault-Accommodating Specification
Fault-Accommodating Controller

Reconfigurator Design

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.

Virtualised Controller
Fault-Accommodating Plant

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.

Inactivity Conditions

The resulting reconfigurator is pictured below.

Reconfigurator

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.

Virtualised Controller 1
Virtualised Controller 2

The respective closed-loop system are shown below

Self-Reconfiguring Closed-Loop System 1
Self-Reconfiguring Closed-Loop System 2

Obviously both closed-loop system fulfil the critical liveness properties completeness and non-conflictingness

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"

>>