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
