scholarly journals Extended FRAM by Integrating with Model Checking to Effectively Explore Hazard Evolution

2015 ◽  
Vol 2015 ◽  
pp. 1-11 ◽  
Author(s):  
Guihuan Duan ◽  
Jin Tian ◽  
Juyi Wu
Keyword(s):  
Model Checking ◽  
System Design ◽  
Theory And Practice ◽  
Accident Analysis ◽  
Analysis Method ◽  
Resonance Analysis ◽  
Emergent Phenomenon ◽  
Counter Example ◽  
Model Complex ◽  
Safety Constraints

Functional Resonance Analysis Method (FRAM), which defines a systemic framework to model complex systems from the perspective of function and views accidents as emergent phenomenon of function’s variability, is playing an increasingly significant role in the development of systemic accident theory. However, as FRAM is typically taken as a theoretic method, there is a lack of specific approaches or supportive tools to bridge the theory and practice. To fill the gap and contribute to the development of FRAM, (1) function’s variability was described further, with the rules of interaction among variability of different functions being determined and (2) the technology of model checking (MC) was used for the analysis of function’s variability to automatically search the potential paths that could lead to hazards. By means of MC, system’s behaviors (normal or abnormal) are simulated and the counter example(s) that violates the safety constraints and requirements can be provided, if there is any, to improve the system design. The extended FRAM approach was applied to a typical air accident analysis, with more details drawn than the conclusions in the accident report issued officially by Agenzia Nazionale per la Sicurezza del Volo (ANSV).

Schedulability Analysis for Timed Automata With Tasks

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Jinghao Sun ◽  
Nan Guan ◽  
Rongxiao Shi ◽  
Guozhen Tan ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Real Time ◽  
Timed Automata ◽  
Schedulability Analysis ◽  
Scheduling Theory ◽  
Real Time Scheduling ◽  
Analysis Techniques ◽  
Model Complex ◽  
Time Scheduling

Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.

Distributed CTL model checking using MapReduce: theory and practice

2015 ◽  
Vol 28 (11) ◽  
pp. 3025-3041 ◽  
Author(s):  
Carlo Bellettini ◽  
Matteo Camilli ◽  
Lorenzo Capra ◽  
Mattia Monga
Keyword(s):  
Model Checking ◽  
Theory And Practice

scholarly journals FRAM for Systemic Accident Analysis: A Matrix Representation of Functional Resonance

2018 ◽  
Vol 25 (01) ◽  
pp. 1850001 ◽  
Author(s):  
Patriarca Riccardo ◽  
Del Pinto Gianluca ◽  
Di Gravio Giulio ◽  
Costantino Francesco
Keyword(s):  
Traffic Management ◽  
Critical Role ◽  
Accident Analysis ◽  
Illustrative Case ◽  
Resonance Analysis ◽  
Linear Sequence ◽  
Illustrative Case Study ◽  
User Friendly ◽  
Runway Incursion

Due to the inherent complexity of nowadays Air Traffic Management (ATM) system, standard methods looking at an event as a linear sequence of failures might become inappropriate. For this purpose, adopting a systemic perspective, the Functional Resonance Analysis Method (FRAM) originally developed by Hollnagel, helps in identifying nonlinear combinations of events and interrelationships. This paper aims to enhance the strength of FRAM-based accident analyses, discussing the Resilience Analysis Matrix (RAM), a user-friendly tool that supports the analyst during the analysis, in order to reduce the complexity of representation of FRAM. The RAM offers a two-dimensional representation which systematically highlights the connections among couplings, and thus even the highly connected group of couplings. As an illustrative case study, this paper develops a systemic accident analysis for the runway incursion happened in February 1991 at LAX airport, involving SkyWest Flight 5569 and USAir Flight 1493. FRAM confirms itself a powerful method to characterize the variability of the operational scenario, identifying the dynamic couplings with a critical role during the event and helping in discussing the systemic effects of variability at different level of analysis.

Sign in / Sign up

Export Citation Format

Share Document