GROOVE Tool for Verification Based on Graph Rewriting

Organisation:	RWTH Aachen University (GERMANY) University of Twente (THE NETHERLANDS)
Functionality:	Formal Verification.
Tools used:	DFTCalc CADP (Construction and Analysis of Distributed Processes)
Period:	2015
Description:	Fault tree analysis is one of the most prominent safety assessment technique, standardised by the IEC and deployed by many companies and institutions. Fault trees (FTs) model how failures propagate through the system: FT leaves model component failures and are equipped with continuous probability distributions; FT gates model how component failures lead to system failures. Dynamic fault trees (DFTs) are a well-known extension to standard fault trees that cater for common dependability patterns, such as spare management, functional dependency, and sequencing. Analysis of DFTs relies on extracting an underlying stochastic model and analyzing it using stochastic model checking. Since the order in which the DFT components fail matters, this approach severely suffers from the state space explosion problem. A novel technique is proposed to reduce the state space of DFTs prior to their analysis. The key idea is to consider DFTs as (typed) directed graphs and manipulate them by graph rewriting. The technique was implemented on top of the graph transformation tool GROOVE and the DFT analysis tool DFTCalc, yielding a fully automated tool chain for graph-based DFT reduction and analysis. The DFT is translated into the input format of GROOVE, which applies the graph rewriting rules defined for DFT reduction. The output of GROOVE (i.e., the rewritten graph), is translated back into a DFT that is then analysed by DFTCalc. DFTCalc exploits CADP for compositional state space generation and reduction (using bisimulation minimisation) of the underlying IMC of the DFT. Finally, the resulting Markov chain is analysed for the user-specified measure by the probabilistic model checker MRMC. Several variations of seven benchmarks were analysed, comprised of over 170 fault trees in total, originating from standard examples from the literature as well as industrial case studies from aerospace and railway engineering. Rewriting enabled to cope with 49 DFTs that could not be handled before. For the other fault trees rewriting pays off, being much faster and more memory efficient, up to two orders of magnitude. This comes at no run-time penalty: graph rewriting is very fast and the stochastic model generation is significantly accelerated due to the DFT reduction.
Conclusions:	The novel reduction technique for minimising DFTs using graph rewriting yields drastic savings in terms of time and memory consumption (up to two orders of magnitude). The rewriting approach is applicable too for alternative DFT analysis techniques that isolate static sub-trees. It is also applicable to trees similar to DFTs, e.g., dynamic event/fault trees, extended FTs, and attack trees.
Publications:	[Junges-Guck-Katoen-et-al-15] Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, and Mariëlle Stoelinga. "Fault Trees on a Diet - Automated Reduction by Graph Rewriting". Proceedings of the 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications SETTA'2015, LNCS vol. 9409, pages 3-18. Springer Verlag, November 2015. Available on-line at: http://eprints.eemcs.utwente.nl/26418/01/chp%253A10.1007%252F978-3-319-25942-0_1.pdf or from the CADP Web site in PDF or PostScript [Junges-Guck-Katoen-et-al-17] Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, and Mariëlle Stoelinga. "Fault Trees on a Diet: Automated Reduction by Graph Rewriting". Formal Aspects of Computing 29(4):651-703, July 2017. Available on-line at: http://wwwhome.cs.utwente.nl/~rensink/papers/facs2017.pdf or from the CADP Web site in PDF or PostScript
Contact:	Arend Rensink Formal Methods and Tools Department of Computer Science University of Twente P.O. Box 217 NL-7500 AE Enschede THE NETHERLANDS Tel: +31 (0)53 489 4862 Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr/software

Back to the CADP research tools page