COMPASS

HASDEL Process

The Figure 1 summarizes the HASDEL approach. The engineering teams capture the system architecture thanks to SLIM, a language very close from AADL. SLIM allows modelling the processors, the communication network, the devices (sensors and actuators), the software, etc… When needed, the electrical modes of the equipment (powered, not powered, booting…) and their functional modes are captured by timed finite state machines. The RAMS engineers complete thus this engineering model with specific timed error models and fault injections. This model can then be used to perform RAMS analysis (thanks to model checking, formal proof, generation of timed failure propagation graphs, FTA, FMEA…).

Main Features

The HASDEL modelling is based on an extension of the AADL (“Architecture Analysis Design Language”) language. Once the nominal and error models have been modelled, the System/RAMS Engineer can interact with the following use-cases and activities:

• Loading of nominal and error models. The models are loaded through the COMPASS GUI. The nominal model identifies some parameters for modelling of FDIR, in particular: parameters that are visible for the FDIR component (observable) and the recovery actions (input events).
• Fault injection. It comprises the definition of one or more fault injections that describe how the error behaviour influences the nominal behaviour.
• Model Extension. The model extension is triggered automatically by the HASDEL toolset, when the fault injections have been defined. The result is an extended model which incorporates both nominal and error behaviour.
• TFPG Modelling/Synthesis. The System/RAMS Engineer can use a TFPG to model fault propagation in the system. A TFPG is an abstract view of the extended model that focuses on fault propagation information. A TFPG can also be automatically synthesized by the HASDEL toolset.
• TFPG Validation. Whenever a TFPG is (manually) produced, it can be validated, in order to ensure that it is a correct abstraction of the system it refers to. In particular, it is possible to check whether it is defined on the vocabulary of the original system, if the behaviours of the original system are also admitted by the TFPG (and vice versa), and whether the TFPG contains enough information to diagnose all the faults that are of interest.
• Property Specification. It consists in the specification of properties to be used for further analyses. Properties are entered using property patterns. There are different
• Analysis. It comprises all analyses supported by the HASDEL toolset. In accordance with COMPASS, they are categorized as follows:
  • Correctness
    • Simulation: it comprises random and user-guided simulation
    • Deadlock Checking: it is used to check the presence of deadlocks in the input models
    • Zeno detection: it is used to detect and identify Zeno cycles in the model
    • Timelock detection: it is used to detect timelocks in the model
    • Time divergence detection: it is used to detect time divergent behaviour in the model
    • Model Checking: it is used to verify functional correctness of the model
  • Performability
    • Performability Evaluation: it characteristics of the model
  • Safety
    • FTA: it includes generation of (dynamic) fault trees
    • FMEA: it includes generation of FMEA tables
    • Fault Tolerance Evaluation: it is used to collect and classify information on MCS obtained using FTA on different properties
    • FT Evaluation: it is used to evaluate a fault tree probabilistically
    • FT Verification: it is used to verify a probabilistic property on a fault tree
  • FDIR Effectiveness
    • Fault Detection: it verifies the effectiveness of fault detection, given a diagnoser
    • Fault Isolation: it verifies the effectiveness of fault isolation, given a diagnoser
    • Diagnosability: it checks whether there exists an ideal diagnoser that is able to diagnose a given property, using the observability characteristics of the model
    • Fault Recovery: it is used to check recoverability properties, in order to assess the effectiveness of fault recovery, given a FDIR sub-system
    • Fault Coverage Analysis: this analysis is new in HASDEL; it is used to categorize faults depending on whether they can be detected or recovered from, into different classes

HASDEL Environment

The following figure shows the general workflow in the HASDEL Environment. The main activities and the control flow are as follows:

• The user models nominal and error models, and fault injections
• The extended model is generated
• The user defines some properties, and uses them to perform FTA and FMEA
• FTs and FMEA tables, together with the original models, are used to model (and validate) a TFPG. The output of this activity also includes observability information for the original model.
• The observables are inserted into the original model. In parallel, the user can edit an FDIR model, based on information coming from the TFPG and the previously generated artefacts (FTs, FMEA tables)
• The modified SLIM models (nominal, error, FDIR) and fault injections are used to generate an updated extended model
• The user edits additional properties and uses them to formally analyse the extended model