A Composite Safety Assurance Method for Developing System Architecture Using Model Checking

Author(s):  
Qiang Zhi ◽  
Zhengshu Zhou ◽  
Shuji Morisaki

Assurance case helps analyze the system dependability, but the relationships between system elements and assurance case are generally not clearly defined. In order to make system assurance more intuitive and reliable, this paper proposes an approach that clearly defines the relationships between safety issues and system elements and integrates them using ArchiMate. Also, the proposed method applies model checking to system safety assurance, and the checking results are regarded as evidence of assurance cases. This method consists of four steps: interaction visualization, processes model checking, assurance case creation, and composite safety assurance. The significance of this work is that it provides a formalized procedure for safety-critical system assurance, which could increase the confidence in system safety. It would be expected to make the safety of a system easier to explain to third parties and make the system assurance more intuitive and effective. Also, a case study on an automatic driving system is carried out to confirm the effectiveness of this approach.

2021 ◽  
Vol 11 (7) ◽  
pp. 3127
Author(s):  
Angelo Lerro ◽  
Manuela Battipede

This work deals with the safety analysis of an air data system (ADS) partially based on synthetic sensors. The ADS is designed for the small aircraft transportation (SAT) community and is suitable for future unmanned aerial vehicles and urban air mobility applications. The ADS’s main innovation is based on estimation of the flow angles (angle-of-attack and angle-of-sideslip) using synthetic sensors instead of classical vanes (or sensors), whereas pressure and temperature are directly measured with Pitot and temperature probes. As the air data system is a safety-critical system, safety analyses are performed and the results are compared with the safety objectives required by the aircraft integrator. The present paper introduces the common aeronautical procedures for system safety assessment applied to a safety critical system partially based on synthetic sensors. The mean time between failures of ADS’s sub-parts are estimated on a statistical basis in order to evaluate the failure rate of the ADS’s functions. The proposed safety analysis is also useful in identifying the most critical air data system parts and sub-parts. Possible technological gaps to be filled to achieve the airworthiness safety objectives with nonredundant architectures are also identified.


Author(s):  
Andrew J. Abbate ◽  
Ellen J. Bass

To support safe and effective human-system integration, a safety-critical system should be Complete, Understandable, Robust, Accurate, and Time efficient (CURATe) with respect to the user, interface, device, and environmental context. Using highly automated model checkers, researchers have shown that CURATe-related specifications can be verified early in the design process for a subset of system elements and interactions. This research introduces an extended model checking approach that aims to address all CURATe measures with respect to a broader range of human-integrated system elements: the interface, including documentation, configurable hardware, and control units; the user, including capabilities, actions, and knowledge; the device, including automation, actuators, and transducers; and the environment, including stimuli and constraints that could shape behavior. We describe a concept for what elements/interactions among them need to be modeled formally as well as a concept for applicable CURATe specifications. With respect to these concepts, we propose a formal model architecture and one temporal logic encoding for each CURATe specification.


2018 ◽  
Vol 2018 ◽  
pp. 1-9
Author(s):  
Haonan Feng

VBTC (vehicle-to-vehicle communication based train control) has gradually become an important research trend in the field of rail transit. This has resulted in advantages of decreasing the number of pieces of wayside equipment and improving the efficiency of real-time system communication. Characteristics and mechanism of train-to-train communication, as key implementation technology of safety critical system, are given and discussed. A new method, based on the LTS (labelled transition system) model checking, is proposed for verifying the safety properties in the communication procedure. The LTS method is adapted to model system behaviours; analysis and safety verification are checked by means of LTSA (labelled transition system analyzer) software. The results show that it is an efficient method to verify safety properties, as well as to assist the complex system’s design and development.


2017 ◽  
Vol 27 (1) ◽  
pp. 477-486
Author(s):  
Sarah A. Sheard ◽  
Michael D. Konrad ◽  
Charles B. Weinstock ◽  
William R. Nichols

2019 ◽  
Vol 18 (2) ◽  
pp. 1:1 ◽  
Author(s):  
Romina Eramo ◽  
Florent Marchand de Kerchove ◽  
Maximilien Colange ◽  
Michele Tucci ◽  
Julien Ouy ◽  
...  

Sign in / Sign up

Export Citation Format

Share Document