Combination of Compositional Verification and Model Checking for Safety Assessment of Complex Engineered Systems

2014 ◽  
Author(s):  
Hoda Mehrpouyan ◽  
Dimitra Giannakopoulou ◽  
Irem Y. Tumer ◽  
Chris Hoyle ◽  
Guillaume Brat
Keyword(s):  
Model Checking ◽  
Compositional Analysis ◽  
Compositional Verification ◽  
Safety Properties ◽  
Safety Issues ◽  
Complex Engineered Systems ◽  
System A ◽  
Safety Specification ◽  
Engineered Systems ◽  
Local Safety

This paper presents a novel safety specification and verification approach based on the compositional reasoning and model checking algorithms. The behavioral specification of each component and subsystem is modeled to describe the overall structure of the design. Then, these specifications are analyzed to determine the least number of component redundancies that are required to tolerate and prevent catastrophic system failure. The framework utilizes Labelled Transition Systems (LTS) formalism to model the behavior of components and subsystems. Furthermore, compositional analysis is used to reason about the components’ constraints (or assumptions) on their environments and the properties (or guarantees) of their output. This identification of local safety properties of components and subsystems leads to satisfaction of the desired safety requirements for the global system. A model of quad-redundant Electro-Mechanical Actuator (EMA) is constructed and, in an iterative approach, its safety properties are analyzed. Experimental results confirm the feasibility of the proposed approach for verifying the safety issues associated with complex systems in the early stages of the design process.

Creating Faultable Network Models of Complex Engineered Systems

2014 ◽  
Author(s):  
Brandon M. Haley ◽  
Andy Dong ◽  
Irem Y. Tumer
Keyword(s):  
Failure Analysis ◽  
Network Models ◽  
System Behavior ◽  
Levels Of Abstraction ◽  
Complex Engineered Systems ◽  
System A ◽  
Topological Configuration ◽  
Engineered Systems ◽  
Types Of Faults ◽  
Insight Into

This paper presents a new methodology for modeling complex engineered systems using complex networks for failure analysis. Many existing network-based modeling approaches for complex engineered systems “abstract away” the functional details to focus on the topological configuration of the system and thus do not provide adequate insight into system behavior. To model failures more adequately, we present two types of network representations of a complex engineered system: a uni-partite architectural network and a weighted bi-partite behavioral network. Whereas the architectural network describes physical inter-connectivity, the behavioral network represents the interaction between functions and variables in mathematical models of the system and its constituent components. The levels of abstraction for nodes in both network types affords the evaluation of failures involving morphology or behavior, respectively. The approach is shown with respect to a drivetrain model. Architectural and behavioral networks are compared with respect to the types of faults that can be described. We conclude with considerations that should be employed when modeling complex engineered systems as networks for the purpose of failure analysis.

scholarly journals Compositional Verification using Model Checking and Theorem Proving

2020 ◽  
pp. 305-314
Author(s):  
Diego Marmsoler
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
Embedded Systems ◽  
Theorem Proving ◽  
Formal Modeling ◽  
Compositional Verification ◽  
Modeling And Analysis ◽  
Simple Version ◽  
Evolving Systems ◽  
Alternative Approach

AbstractCollaborative embedded systems form groups in which individual systems collaborate to achieve an overall goal. To this end, new systems may join a group and participating systems can leave the group. Classical techniques for the formal modeling and analysis of distributed systems, however, are mainly based on a static notion of systems and thus are often not well suited for the modeling and analysis of collaborative embedded systems. In this chapter, we propose an alternative approach that allows for the verification of dynamically evolving systems and we demonstrate it in terms of a running example: a simple version of an adaptable and flexible factory.

scholarly journals Forensic Engineering Use Of Fault Tree Analysis

2006 ◽  
Vol 23 (2) ◽  
Author(s):  
Frank H. Johnson ◽  
DeWitt William E.
Keyword(s):  
Fault Tree ◽  
Fault Tree Analysis ◽  
Tree Analysis ◽  
Complex Engineered Systems ◽  
Track Record ◽  
Forensic Engineering ◽  
Fire And Explosion ◽  
Engineered Systems ◽  
Analytical Tools

Analytical Tools, Like Fault Tree Analysis, Have A Proven Track Record In The Aviation And Nuclear Industries. A Positive Tree Is Used To Insure That A Complex Engineered System Operates Correctly. A Negative Tree (Or Fault Tree) Is Used To Investigate Failures Of Complex Engineered Systems. Boeings Use Of Fault Tree Analysis To Investigate The Apollo Launch Pad Fire In 1967 Brought National Attention To The Technique. The 2002 Edition Of Nfpa 921, Guide For Fire And Explosion Investigations, Contains A New Chapter Entitled Failure Analysis And Analytical Tools. That Chapter Addresses Fault Tree Analysis With Respect To Fire And Explosion Investigation. This Paper Will Review The Fundamentals Of Fault Tree Analysis, List Recent Peer Reviewed Papers About The Forensic Engineering Use Of Fault Tree Analysis, Present A Relevant Forensic Engineering Case Study, And Conclude With The Results Of A Recent University Study On The Subject.

scholarly journals Design of Complex Engineered Systems

2010 ◽  
Vol 132 (12) ◽  
Author(s):  
Christina L. Bloebaum ◽  
Anna-Maria R. McGowan
Keyword(s):  
Complex Engineered Systems ◽  
Engineered Systems

Simultaneous SAT-Based Model Checking of Safety Properties

2006 ◽  
pp. 56-75 ◽  
Author(s):  
Zurab Khasidashvili ◽  
Alexander Nadel ◽  
Amit Palti ◽  
Ziyad Hanna
Keyword(s):  
Model Checking ◽  
Safety Properties

Quantifying the Resilience-Informed Scenario Cost Sum: A Value-Driven Design Approach for Functional Hazard Assessment

2018 ◽  
Vol 141 (2) ◽  
Author(s):  
Daniel Hulse ◽  
Christopher Hoyle ◽  
Kai Goebel ◽  
Irem Y. Tumer
Keyword(s):  
Functional Model ◽  
Scoring Function ◽  
Modeling Languages ◽  
Concept Selection ◽  
Complex Engineered Systems ◽  
Propagation Behavior ◽  
Engineered Systems ◽  
Selection Framework ◽  
And Function ◽  
Probability Information

Complex engineered systems can carry risk of high failure consequences, and as a result, resilience—the ability to avoid or quickly recover from faults—is desirable. Ideally, resilience should be designed-in as early in the design process as possible so that designers can best leverage the ability to explore the design space. Toward this end, previous work has developed functional modeling languages which represent the functions which must be performed by a system and function-based fault modeling frameworks have been developed to predict the resulting fault propagation behavior of a given functional model. However, little has been done to formally optimize or compare designs based on these predictions, partially because the effects of these models have not been quantified into an objective function to optimize. The work described herein closes this gap by introducing the resilience-informed scenario cost sum (RISCS), a scoring function which integrates with a fault scenario-based simulation, to enable the optimization and evaluation of functional model resilience. The scoring function accomplishes this by quantifying the expected cost of a design's fault response using probability information, and combining this cost with design and operational costs such that it may be parameterized in terms of designer-specified resilient features. The usefulness and limitations of using this approach in a general optimization and concept selection framework are discussed in general, and demonstrated on a monopropellant system design problem. Using RISCS as an objective for optimization, the algorithm selects the set of resilient features which provides the optimal trade-off between design cost and risk. For concept selection, RISCS is used to judge whether resilient concept variants justify their design costs and make direct comparisons between different model structures.

Evaluation of System Reconfigurability Based on Usable Excess

2014 ◽  
Author(s):  
Jeffrey D. Allen ◽  
Jason D. Watson ◽  
Christopher A. Mattson ◽  
Scott M. Ferguson
Keyword(s):  
Communication Systems ◽  
Assembly Line ◽  
Assembly Lines ◽  
Automated Assembly ◽  
Complex Engineered Systems ◽  
Future Needs ◽  
Key Factor ◽  
Long Time ◽  
Engineered Systems ◽  
Over Time

The challenge of designing complex engineered systems with long service lives can be daunting. As customer needs change over time, such systems must evolve to meet these needs. This paper presents a method for evaluating the reconfigurability of systems to meet future needs. Specifically we show that excess capability is a key factor in evaluating the reconfigurability of a system to a particular need, and that the overall system reconfigurability is a function of the system’s reconfigurability to all future needs combined. There are many examples of complex engineered systems; for example, aircraft, ships, communication systems, spacecraft and automated assembly lines. These systems cost millions of dollars to design and millions to replicate. They often need to stay in service for a long time. However, this is often limited by an inability to adapt to meet future needs. Using an automated assembly line as an example, we show that system reconfigurability can be modeled as a function of usable excess capability.

Sign in / Sign up

Export Citation Format

Share Document