We present a comprehensive methodology for the specification and analysis of critical embedded systems. The methodology is based on an architectural design language that enables modeling of both software and hardware components, timed and hybrid behavior, faulty behavior and degraded modes of operation, error propagation and recovery. The methodology is supported by an integrated platform, implemented on top of state-of-the-art tools, that provides verification capabilities ranging from requirements analysis to functional verification, safety assessment, performability evaluation, diagnosis and diagnosability.
The design of critical embedded systems is a very complex and highly challenging task, for a number of reasons. First, it requires designing and assembling heterogeneous components, implemented either in hardware or in software, and their interactions. Secondly, it has to take into account functional requirements as well as several sorts of non-functional requirements, such as (real-)time constraints, performability and safety requirements.
In this paper we present a comprehensive and tool-supported methodology for the design of critical systems, following the component-based paradigm. Component-based design helps to master design complexity while, at the same time, allowing for reusability. The key principle is a clear distinction between component behavior (implementation) and the interactions between the individual components (interfacing). The internal structure of a component implementation is specified by its decomposition into subcomponents, together with their hardware/software bindings and their interaction via connections over ports.
The design methodology is built on top of the SLIM modeling language, an
architectural language inspired by SAE’s AADL [
Funded by ESA/ESTEC under Contract No. 21171/07/NL/JD
reconfiguration of components and port connections, and probabilistic error
behavior and propagation, while enriching it with constructs to express timed and
hybrid behavior. Moreover, the SLIM language is endowed with a formal
semantics that cover all of its aspects in a clear and unambiguous way [
The methodology proposed in this work is targeted at the architectural design of critical embedded systems, and in particular it covers modeling and verification of the following aspects: requirements analysis, verification of functional correctness, safety assessment and fault tolerance measures, quantitative and performability analysis, and partial observability analysis, including effectiveness of the FDIR (Fault Detection, Identification and Recovery) components.
The proposed approach is being investigated in the COMPASS project3 (Correctness, Modeling, and Performance of Aerospace Systems) in the aerospace domain, and results as a response to an invitation to tender by the European Space Agency. The techniques described in this work, however, are applicable in general to every domain where design of critical embedded systems is involved.
The paper is structured as follows. In Section 2 we describe the main features of the SLIM language; in Section 3 we give an overview of the methodology; in Section 4 we discuss the COMPASS tool, implementing the methodology, and finally we draw some conclusions and discuss future directions in Section 5. 2
The SLIM language follows the component-based paradigm. In SLIM, it is possible to refer to both software (e.g. threads and processes) and hardware components (e.g. memories and processors) as first-class objects. Each component is given via its type, describing the interface, and its implementation, describing the interactions via a finite state automaton. Sets of interacting components can be grouped into composite components, enabling the modeler to manage the system’s complexity by introducing a component hierarchy. Communication is achieved via exchange of messages on event ports, in a rendez-vous manner. Moreover, components may exchange data through typed data ports (e.g. bool, integer and real data types). Timed and hybrid behavior can be expressed by means of real-valued variables with (linear) time-dependent dynamics.
The resulting hierarchical system model, also referred to as nominal model,
describes the system behavior under normal operation. This is complemented
by an error model which expresses how the system can fail. Moreover, a subset
of the nominal components may be designated as dealing with error diagnosis
and recovery; they are referred to as FDIR (Fault Detection, Identification and
Recovery). The error model expresses how faults may affect normal operation
and may lead the system into a degraded mode of operation. It is modeled as
a probabilistic finite state automaton, where transitions may occur due to error
events which may be annotated with a rate that indicates the expected number
of occurrences per time unit. Transitions can also occur because of error
propagations from other components. The nominal and error models are linked through
3 http://compass.informatik.rwth-aachen.de
a so-called fault injection. A fault injection expresses the effect of the occurrence
of the corresponding error on the nominal model. Multiple fault injections are
possible. The process of integrating the nominal models with the error models
and the fault injections, is called model extension [
We refer to [
The methodology discussed in this paper is inspired by the framework described
in [
Safety analysis investigates the behavior of a system in degraded conditions,
that is, when some parts of the system are not working properly due to
malfunctions. It includes hazard analysis, whose goal is to identify all the hazards
of the system and ensure that the system meets the safety requirements that
are required for its deployment and use. Examples of hazard analysis techniques
are Fault Tree Analysis (FTA) and Failure Mode and Effects Analysis (FMEA).
Model-based safety analysis is in turn based on model checking techniques [
Quantitative analysis and performability aim at evaluating system performance with respect to timed and probabilistic requirements. They also include probabilistic versions of safety and diagnosability measures. The related requirements can be expressed in Continuous Stochastic Logic (CSL). The implementation of these analyses is based on probabilistic model checking techniques.
Diagnosis can be seen as the problem of safety analysis carried out at runtime. It is usually performed on systems which provide limited run-time sensing, and under the hypothesis of partial observability. Diagnosis starts from the observed run time behavior of a system, and tries to provide an explanation (in terms of hidden states). In particular, diagnosis is often the problem of identifying the set of possible causes of a specific unexpected or faulty behavior. Probabilistic information can be taken into account, in order to search for the most likely explanation. Another related problem is diagnosability, i.e., the analysis, at design time, of diagnosis capabilities. Finally, the problem of synthesis consists in the automatic generation of controllers from specifications. The latter problem has been tackled by planning techniques based on model checking.
Finally, requirements validation is used to check correctness and completeness of a set of properties. Requirements validation is performed before the system architectural design starts, and has the goal of ensuring the quality of system requirements. In particular, our approach enables checking for logical consistency, i.e., freedom from contradictions. Moreover, it is possible to check whether a given set of properties is strict enough to rule out unwanted behavior, and not too strict to disallow for certain desirable behavior. 4
The methodology is supported by an integrated toolset, which is built on top of
existing state-of-the-art tools for formal verification, based on model checking. In
particular, the toolset builds upon the NuSMV [
A few building blocks itnagkemcoadreel eoxftpenersfioornm,t-rans- S−−AANFDFMAyEnLETaYAmYSiTcISaFbaleuslt Trees MSloidmel PPraotpteerrnty −−RVEAPPQrrLooUIppDeeIRArrttEyyTMISAOiEsmNsNuurTlaaSnticoen lating the SLIM input model into NuSMV and Symbol MRMC formats when Table InPsrtoapnteirattyor tnreaecdeesda,nadnfdauvlitsutraeliezse. ExMteondseioln SIlinmstaPnrtoiapteorrty
The following anal- Slim2SMV RAT
yses are supported.
Requirements validation NuSMV SMV2Sigref Sigref2MRMC MRMC
is used to analyse the
quality (correctness and
completeness) of the SMV2Slim SigRef
requirements, and is car- VTireawceer FaVuiletwTerree
ried out by the RAT
itfiocoal.tiConorfroeccutsneesssonvevre-r- −−CVOEPSRirRmoIRpFueEIlraCCttyAiTovTNneIErOiSfNiScation −−DAINFSAyDAGnILtRNhYeOeSsfSiIfsSeAcoBtfiIvOLebInTseeYsrsvmabeialistuyrResequirements P−−AENPPRreAorFfLbOoaYrRbmSiMlIaiSsbAtiilBcitIfyLaumITlteYatrseuerses
ification of functional
requirements, and is
implemented on top of Fig. 1. Architecture of the toolset.
NuSMV; NuSMV implements standard symbolic model checking techniques such
as BDD-based and SAT-based (bounded) model checking, as well as SMT
(Satisfiability Modulo Theory)-based techniques to deal with hybrid models. Safety
analysis supports two of the most popular hazard analysis techniques, namely
FTA and FMEA, that are carried out by FSAP [
In this paper we have presented a comprehensive methodology and a toolset for the specification and analysis of critical embedded systems, that focuses on system features such as (real-)time and faulty behavior, degraded modes of operation, diagnosis and performability. The methodology and toolset are currently being evaluated on industrial-size case studies from the aerospace domain, that will provide a substantial insight into their applicability and effectiveness.
Our methodology is applicable to any domain where, e.g., timing, system performance and safety are at stake. Examples are avionics, transportation, including railways and automotive, power plants, and the medical domain. Our approach is based on a general purpose architectural language, and it is especially targeted at modeling and analyzing systems designs at the architectural level. It can be complemented by specific implementation-level languages to deal with the most implementation-oriented features of system design.
The toolset is under active development and evaluation. A thorough experimental evaluation is planned, based on a comprehensive set of case studies.
Finally, some of the modifications to the AADL language that have been incorporated into SLIM, have been brought into the AADL standardization bodies for evaluation and proposed as a possible extension of the standard.