CORAL (COmpositional Reliability and Availability anaLysis)

Organisation:	University of Saarbrücken (GERMANY) University of Twente (THE NETHERLANDS)
Functionality:	Reliability and availability analysis.
Tools used:	CADP (Construction and Analysis of Distributed Processes) Dynamic Fault Trees (DFT)
Period:	2007-2009
Description:	Reliability and availability measures, such as system failure probability during a given mission time and system mean-time-between-failures, are often important measures to assess in embedded system design. Dynamic fault trees (DFTs) are a graphical, high-level and versatile formalism to analyze the reliability of computer-based systems, describing the failure of the system in terms of the failures of its components. A DFT is comprised of basic events (modeling the failure of the physical components) and gates (modeling how component failures induce system failures). Typically, a DFT is analyzed by first converting it into a continuous-time Markov chain (CTMC) and then by computing the reliability measures from this CTMC. Although DFTs have been experiencing a growing success among reliability engineers, a number of issues persists when using DFTs: lack of formal semantics, of modular analysis and modular model building. This work provides a formal semantics to DFTs by translating them into input/output interactive Markov chains (I/O-IMCs), which are an extension of CTMCs with discrete input, output, and internal actions. The semantics is fully compositional, meaning that the semantics of a DFT is expressed in terms of the semantics of its elements, using the parallel composition operator available for I/O-IMCs. This enables an efficient analysis of DFTs through compositional aggregation, which helps to alleviate the state space explosion problem by incrementally building the DFT state space. This methodology was implemented in a tool named CORAL (COmpositional Reliability and Availability anaLysis), which uses the CADP toolbox. CORAL proceeds in three steps: (1) The DFT is translated into a group of I/O-IMC models, one for each DFT element; (2) These I/O-IMCs are iteratively composed, abstracted and aggregated until a single I/O-IMC model is obtained; (3) The resulting I/O-IMC model is translated into a CTMC, on which transient analysis is performed using the BCG_TRANSIENT tool of CADP.
Conclusions:	The compositional semantics proposed allows the DFT formalism to be easily extended or modified (e.g., by adding repairable components). Future work on the CORAL tool includes the study of heuristics for determining a composition order of intermediate I/O-IMCs in order to reduce the size of intermediate models produced during translation.
Publications:	[Boudali-Crouzen-Stoelinga-08] Hichem Boudali, Pepijn Crouzen, and Mariëlle Stoelinga. "CORAL - A Tool for Compositional Reliability and Availability Analysis". In Proceedings of the ARTIST workshop: Tool Platforms for Embedded Systems Modeling, Analysis and Validation. Satellite event of the 19th International Conference on Computer Aided Verification CAV'2007 (Berlin, Germany), July 2007. Full version available on-line at: http://wwwhome.cs.utwente.nl/~marielle/papers/BCS07c.pdf or from the CADP Web site in PDF or PostScript [Boudali-Crouzen-Stoelinga-09] Hichem Boudali, Pepijn Crouzen, and Marielle Stoelinga. "A Rigorous, Compositional, and Extensible Framework for Dynamic Fault Tree Analysis". IEEE Transactions on Dependable and Secure Computing 99(1), 2009. Available on-line at: http://www.vf.utwente.nl/~marielle/papers/BCS09.pdf or from the CADP Web site in PDF or PostScript
Contact:	Mariëlle Stoelinga Dept. of Computer Science Formal Methods & Tools P.O. Box 217 7500 AE Enschede The Netherlands Tel: +31 53 489 3773 Fax: +31 53 489 3247 Email: marielle@cs.utwente.nl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page