Qualitative analysis for state/event fault trees using formal model checking

doi:10.21629/JSEE.2019.05.13

Journal of Systems Engineering and Electronics ›› 2019, Vol. 30 ›› Issue (5): 959-973.doi: 10.21629/JSEE.2019.05.13

• Systems Engineering • Previous Articles Next Articles

Qualitative analysis for state/event fault trees using formal model checking

Quan JIANG^1,²(), Chunling ZHU^1,*(), Siqi WANG¹()

¹ College of Aerospace Engineering, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
² China Academy of Electronics and Information Technology, Beijing 100083, China

Received:2018-09-10 Online:2019-10-08 Published:2019-10-09
Contact: Chunling ZHU E-mail:jiangquan@nuaa.edu.cn;clzh@nuaa.edu.cn;wangsq@nuaa.edu.cn
About author:JIANG Quan was born in 1981. She is a doctor candidate in Nanjing University of Aeronautics and Astronautics, majoring in man-machine and environmental engineering. Her main research interests are embedded system fault analysis, system safety analysis, and formal verification and validation. E-mail: jiangquan@nuaa.edu.cn|ZHU Chunling was born in 1968. She is a professor in Nanjing University of Aeronautics and Astronautics, and her research lies in the fields of aircraft environment control, aircraft icing and protection, airborne equipment cooling, with a particular focus on man-machine and environmental engineering. E-mail: clzh@nuaa.edu.cn|WANG Siqi was born in 1990. She graduated from Nanjing University of Aeronautics and Astronautics in 2016, majoring in software engineering. And now she works in Huawei Company, mainly responsible for the safety design and analysis of electronic products. Her research interests include system modeling, requirement verification, and formal model checking. E-mail: wangsq@nuaa.edu.cn
Supported by:
the National Natural Science Foundation of China(11832012);This work was supported by the National Natural Science Foundation of China (11832012)

Abstract

Abstract:

A state/event fault tree (SEFT) is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems. Such systems are ubiquitous in all areas of everyday life, and safety and reliability analyses are increasingly required for these systems. SEFTs combine elements from the traditional fault tree with elements from state-based techniques. In the context of the real-time safety-critical systems, SEFTs do not describe the time properties and important time-dependent system behaviors that can lead to system failures. Further, SEFTs lack the precise semantics required for formally modeling time behaviors. In this paper, we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata (TA), and use the model checker UPPAAL to verify system requirements' properties. The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems. Finally, we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.

Key words: state/event fault tree (SEFT), timed automata (TA), model transformation, safety analysis

Quan JIANG, Chunling ZHU, Siqi WANG. Qualitative analysis for state/event fault trees using formal model checking[J]. Journal of Systems Engineering and Electronics, 2019, 30(5): 959-973.

Figures/Tables 12

Fig 1

Table 1

Fig 2

Fig 3

Fig 4

Table 2

Fig 5

Fig 6

Fig 7

Fig 8

Fig 9

Fig 10

References 23

1	DASKAYA I, HUHN M, MILIUS S. Formal safety analysis in industrial practice. Proc. of the International Conference on Formal Methods for Industrial Critical Systems, 2011, 68- 84.
2	KAISER B, GRAMLICH C. State-event-fault-trees-a safety analysis model for software controlled systems. Reliability Engineering&System Safety, 2007, 92 (11): 1521- 1537.
3	CHENG Y H, JIANG L, JIANG B, et al. Useful life prediction using a stochastic hybrid automata model for an ACS multigyro subsystem. Journal of Systems Engineering and Electronics, 2019, 30 (1): 154- 166. doi: 10.21629/JSEE.2019.01.15
4	SONG B, ZHOU Z, MA C, et al. Reliability analysis of monotone coherent multi-state systems based on Bayesian networks. Journal of Systems Engineering and Electronics, 2016, 27 (6): 1326- 1335. doi: 10.21629/JSEE.2016.06.20
5	LAN J, YUAN H J, XIA J. Improved method for dynamic fault tree analysis based on discrete-time Bayesian network. Systems Engineering and Electronics, 2018, 40 (4): 948- 953.
6	ČEPIN M, MAVKO B. A dynamic fault tree. Reliability Engineering&System Safety, 2002, 75 (1): 83- 91.
7	JIN G D, LU L B. System of developing scale modeling and simulation for URAV. Journal of Systems Engineering and Electronics, 2008, 19 (6): 1295- 1300. doi: 10.1016/S1004-4132(08)60233-9
8	ROTH M, HARTOYO A, LIGGESMEYER P. Efficient reachability graph development for qualitive analysis of state/event fault trees. Proc. of the IEEE International Symposium on Software Reliability Engineering Workshops, 2015, 144- 151.
9	ROTH M, LIGGESMEYER P. Qualitative analysis of state/event fault trees for supporting the certification process of software-intensive systems. Proc. of the IEEE International Symposium on Software Reliability Engineering Workshops, 2013, 353- 358.
10	KABIR S. An overview of fault tree analysis and its application in model based dependability analysis. Expert Systems with Applications, 2017, 77, 114- 135. doi: 10.1016/j.eswa.2017.01.058
11	BOUDALI H, CROUZEN P, STOELINGA M. Dynamic fault tree analysis using input/output interactive Markov chains. Proc. of the IEEE/IFIP International Conference on Dependable Systems and Networks, 2007, 708- 717.
12	DAL LAGO L, FERRANTE O, PASSERONE R, et al. Dependability assessment of SOA-based CPS with contracts and model-based fault injection. IEEE Trans. on Industrial Informatics, 2018, 14 (1): 360- 369. doi: 10.1109/TII.2017.2689337
13	WEI Q, JIAO J, ZHAO T. Flight control system failure modeling and verification based on SPIN. Engineering Failure Analysis, 2017, 82, 501- 513. doi: 10.1016/j.engfailanal.2017.04.004
14	IGLESIA D G D L, WEYNS D. MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. on Autonomous and Adaptive Systems, 2015, 10(3): 1-30.
15	XU B, HUANG Z, HU J, et al. Minimal cut sequence generation for state/event fault trees. Proc. of the ACM Middleware Doctoral Symposium, 2013, DOI: 10.1145/2541534.2541592.
16	FEILER P, DELANGE J. Automated fault tree analysis from AADL models. ACM SIGAda Ada Letters, 2017, 36 (2): 39- 46. doi: 10.1145/3092893.3092900
17	GHADHAB M, JUNGES S, KATOEN J P, et al. Safety analysis for vehicle guidance systems with dynamic fault trees. Reliability Engineering&System Safety, 2019, 186, 37- 50.
18	VOLK M, JUNGES S, KATOEN J P. Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. on Industrial Informatics, 2018, 14 (1): 370- 379. doi: 10.1109/TII.2017.2710316
19	DING Y, LI W, ZHONG D, et al. System states transition safety analysis method based on FSM and NuSMV. Proc. of the 2nd International Conference on Management Engineering, Software Engineering and Service Sciences, 2018: 107-112.
20	VILLANI E, PONTES R P, CORACINI G K, et al. Integrating model checking and model based testing for industrial software development. Computers in Industry, 2019, 104, 88- 102. doi: 10.1016/j.compind.2018.08.003
21	WANG L S, LI S J, WEI O H, et al. An automated fault tree generation approach with fault configuration based on model checking. IEEE Access, 2018, 6, 46900- 46914. doi: 10.1109/ACCESS.2018.2863696
22	GERD B, ALEXANDRE D, KIM G. A tutorial on UPPAAL 4.0. Department of Computer Science, 2006, 4(12): 200-236.
23	IGLESIA D G D L, WEYNS D. MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. on Autonomous and Adaptive Systems, 2015, 10(3): 1-31.

State machine	TA	Instruction
StateMachine	TimedAutomata	Mapping to a TA.
Pseudostate	Initial	Expressed as the initial state.
State	Location	Indicates the status of the system.
Transition	Transition	Corresponds to changes that cause state changes.
Constraint	Label	Constraint can represent state constraints. Because it is an expression in the TA, mapping to Label. According to whether the object of Constraint is a State or a Transition, the Label also represents the invariant of Location or the guard of Transition.
OpaqueBehavior	Label	The text attribute of the object's body attribute indicates the change caused by the transition, that is, the expression Exception in Label.
Trigger	Action	The trigger triggered by the trigger maps to Action, and the Trigger maps to Synchronisation, which indicates the operation of the transition synchronization. This allows us to define synchronization events for different TA.

[1]	Jianbo HU, Lei ZHENG, Shukui XU. Safety analysis of wheel brake system based on STAMP/STPA and Monte Carlo simulation [J]. Journal of Systems Engineering and Electronics, 2018, 29(6): 1327-1339.
[2]	Wei Jiang, Hongli Wang, Jinghui Lu, and Zheng Xie. HOSVD-based LPV modeling and mixed robust H2/H∞ control design for air-breathing hypersonic vehicle [J]. Systems Engineering and Electronics, 2016, 27(1): 183-.

Qualitative analysis for state/event fault trees using formal model checking

RichHTML

PDF (PC)

Knowledge

Abstract

Cite this article

Share this article

Figures/Tables 12

References 23

Related Articles 2

Recommended Articles

Metrics

Comments