Qualitative Analysis of State/Event Fault Trees Based on Interface Automata

State/Event Fault Tree (SEFT) can be used for safety modeling and assessment. However, SEFT does not provide adequate semantics for analyzing the minimal scenarios leading to system failures. In this paper, we propose a novel qualitative analysis method for SEFT based on interface automata. Firstly, we propose the concept of guarded interface automata by adding guards on interface automata transitions. Based on this model, we can describe the triggers and guards of SEFT simultaneously. Then, a weak bisimilarity operation is defined to alleviate the state space explosion problem. Based on the proposed guarded interface automata and the weak bisimilarity operation, the semantics of SEFT can be precisely determined. After that, a qualitative analysis process is presented on the basis of the formal semantics of SEFT, and the analyzing result is the minimal cut sequence set representing the causes of system failures. Finally, a fire protection system case study is illustrated step by step to demonstrate the effectiveness of our method.

Interface Automata for Shared Memory

Interface theories based on Interface Automata (IA) are formalisms for the component-based specification of concurrent systems. Extensions of their basic synchronization mechanism permit the modelling of data, but are studied in more complex settings involving modal transition systems or do not abstract from internal computation. In this article, we show how de Alfaro and Henzinger’s original IA theory can be conservatively extended by shared memory data, without sacrificing simplicity or imposing restrictions. Our extension IA for shared Memory (IAM) decorates transitions with pre- and post-conditions over algebraic expressions on shared variables, which are taken into account by IA’s notion of component compatibility. Simplicity is preserved as IAM can be embedded into IA and, thus, accurately lifts IA’s compatibility concept to shared memory. We also provide a ground semantics for IAM that demonstrates that our abstract handling of data within IA’s open systems view is faithful to the standard treatment of data in closed systems.