• libFAUDES
• Reference  
• Type Index  
• Function Index  
• Literature  
•  
• Sections
• CoreFaudes  
  • CoreFaudes
  • Introduction
  • Generators
  • Alphabets
  • Reachability
  • Boolean Operations
  • Regular Expressions
  • Synchronous Composition
  • Projection
  • StateSet Conversion
  • Elementary Types
  • Miscellaneous
  • Vector Types
• CoordinationControl  
• Diagnosis  
  • Diagnosis
  • Introduction
  • Event-Diagnosis
  • Language-Diagnosis
  • Modular Diagnosis
  • Decentralized Diagnosis
  • Application Example
• FaultTolerantControl  
  • FaultTolerantControl
  • Introduction
  • Example
  • Fault-Accommodation
  • Reconfiguration
  • Fault-Patterns
• HioSys  
  • HioSys
  • Introduction
  • Step-By-Step
  • Synthesis Procedure
  • Liveness Properties
  • Application Example
• IoSystem  
  • IoSystem
  • Introduction
  • Properties
  • Synthesis
• Multitasking  
  • Multitasking
  • Introduction
  • Functions
  • Observer
  • Optimal Color Set
  • Reachability
  • Synthesis
• Observer  
  • Observer
  • Introduction
  • Verification
  • Synthesis
  • Example
• Simulator  
  • Simulator
  • Introduction
  • Executor Classes
  • Hardware-In-The-Loop
  • IO-Devices
  • Simulator Interconnection
• Synthesis  
  • Synthesis
  • Introduction
  • Controllability
  • Normality
  • Omega-Controllability
  • Misc Functions
•  
• Types
• Diagnoser  
• FailureTypeMap  
•  
• Functions
• DecentralizedDiagnoser  
• DecentralizedModularDiagnoser  
• EventDiagnoser  
• IsCoDiagnosable  
• IsEventDiagnosable  
• IsIndicatorEventDiagnosable  
• IsLanguageDiagnosable  
• IsLoopPreservingObserver  
• IsModularDiagnosable  
• LanguageDiagnoser  
• LoopPreservingObserver  
• ModularDiagnoser  
•  

Modular Diagnosis

For further illustration, we now study a small application example that consists of two components of our Fischertechnik manufacturing system model in the context of modular diagnosis and decentralized diagnosis. The relevant part of the system is depicted in the following picture.

Component SF (Stack feeder) and C1 (Conveyor belt C1)

Basic Description of the System

The SF comprises a tower that can hold wooden parts and a belt that can move parts until they reach the neighboring conveyor belt C1 (event pass). A light barrier detects if parts arrive at or leave the belt of SF which is modeled by the events sfa and sfl, respectively. In addition, the belt of the SF can start and stop moving (events sfmv and sfs). Its motion is initiated by the event sf-c1 that is shared with C1. The desired behavior of SF according to a previously performed supervisor design is given by the automaton D_SF. Similarly, the desired behavior of C1 is characterized by the automaton D_C1. After the transport of a part is initiated by sf-c1, C1 starts to move (c1mv). As soon as the part arrives at the sensor of C1 (c1a), C1 stops (c1s) and becomes ready for a new transport whenever the part is removed from C1 (c1l).

Component D_SF (Specifiation K_SF)
Component D_C1 (Specification K_C1)

Modular Diagnosis

The faulty behavior of both components is modeled the two component automata G_SF and G_C1 in the subsequent figure. In particular, the event f_pjm in G_SF represents the situation, where the stack feeder is jammed such that no part can leave anymore. Moreover, the event f_pfd in G_C1 models that a part falls from the conveyor belt and thus cannot arrive at the sensor of C1. In both cases, the additional timer events t_sf and t_c1 capture an unusually long passage of time. The corresponding specification automata are shown in the figure above. In this application example, all events except for the failures f_pjm, f_pfd and the shared event pass are observable.

Component G_SF
Local specification K_SF
Component G_C1
Local specification K_C1

Our goal is now to perform modular diagnosis in order to detect the potential failures in the system components SF and C1. That is, we require that SF can detect the occurrence of f_pjm based on its own observation, while C1 is able to find out if f_pfd happened only using the observable events of C1. To this end, we use the function IsModularDiagnosable which confirms that the system is modularly diagnosable.

In addition, we compute the moduar diagnosers for both system components with the function ModularDiagnoser. The resulting diagnoser automata are shown in the figure below. It is readily observed that the diagnoser for SF detects the occurrence of a failure as soon as the timer event t_sf happens, while C1 can uniquely resolve the occurrence of f_pfd after the occurrence of the timer event t_c1.

Diagnoser for G_SF
Diagnoser for G_C1

Decentralized Diagnosis

For the decentralized diagnosis example, the faulty behavior of both components is modeled the two component automata G_SF and G_C1 in the subsequent figure. In particular, the event diag in G_SF represents the situation, where a part is not put correctly but is located diagonally with respect to the direction of the belt. In that case, the belt will periodically lift the part, triggering the events sfl and sfa, whereas the part never arrives at C1. Moreover, the event block in G_C1 models that a part cannot be transported by the SF but is blocked at its initial position. Considering C1, the additional timer event timer captures the case where too much time passes after the occurrence of c1mv. In this application example, the events block and diag are unobservable.

Component G_SF
Component G_C1

Our goal is now to perform modular decentralized diagnosis in order to detect the potential failures in the system components SF and C1. That is, we require that the possible failures can be detected by any of the two local sites SF or C1. Different from modular diagnosis as described above, it is not required that both failures that occur in the component SF are also detected by the corresponding local diagnoser for SF. We use the function IsCoDiagnosable which confirms that the system is co-diagnosable.

In addition, we compute the moduar decentralized diagnosers for both system components with the function DecentralizedModularDiagnoser. The resulting diagnoser automata are shown in the figure below. It is readily observed that the diagnoser for SF detects the occurrence of the failure diag as soon as sfl happens directly after sfa, while C1 can uniquely resolve the occurrence of block after the occurrence of the timer event timer.

Diagnoser for G_SF
Diagnoser for G_C1

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