SURVIVABILITY OF SHIPS AT SEA: A PROPOSED MODEL TO ACCOUNT FOR HUMAN FACTORS IN A SAFETY-CRITICAL SYSTEM

Most serious accidents at sea are caused by minor incidents that escalated into an uncontrolled situation. This study is aiming to develop a model to investigate the likelihood of fatal accidents, given that a critical incident has already occurred. The focus of the study is on human behaviour, adopting a hardware reliability perspective. The vessel is considered as a safety-critical system to be protected by several barriers. The crew role is modelled as active barriers and distinguishing between different functions: perception, decision and action. A Markov approach is proposed to model different situations on the vessel. A mathematical model to estimate the probability of failure in an emergency situation is formulated. A new parameter is defined for the survivability of a vessel, given that a critical incident has taken place. The methods were applied to examine ship-platform collisions cases and the results show strong benefits for diagnosing and evaluating accidents from a human factors perspective as well as for training purposes.

A Framework for Model and Verification of Safety-Critical Operating System Based on ARINC653

As the scale and complexity of safety-critical software continue to grow, it is necessary to ensure safety and reliability to avoid minor errors leading to catastrophic disasters. Meantime, the traditional method, such as testing and simulation alone is insufficient to ensure the correctness of systems. This leads to using formal methods to provide sufficient evidence for systems. However, design a high assurance safety-critical system by formal methods is challenging due to the complexity of operating systems. In addition, the traditional interactive theorem prover used in system verification requires hand-written proofs, which are more expensive. Therefore, the efforts of providing a standardized formal framework as well as safety proofs, are notable for the develop a safety-critical system. The purpose of this paper is to provide a safety framework to establish a highly reliable and safety-critical operating system based on the ARINC653 standard, a multilevel and standardized formal model. To verify the functional correctness of this model, we propose a context-based formal proof method for programs. To achieve this goal, we first model 57 core services of ARINC653 and define the high-level requirements as pre-and post-conditions. Then, we construct a set of specification statements a formal axiom system transformed into logical sentences, and the core service model is transformed into a logical sentence sequence to be proved. Finally, a context-based formal proof system for specification correctness is developed. We have verified the correctness of safety-critical operating system core services with this system. Experience shows that the verification system we developed can be achieved the functional correctness of a complete OS with a low implement burden, and that can simplify the difficulty of automated verification and increase the degree of automation of proof.

Bayesian optimization with safety constraints: safe and automatic parameter tuning in robotics

Selecting the right tuning parameters for algorithms is a pravelent problem in machine learning that can significantly affect the performance of algorithms. Data-efficient optimization algorithms, such as Bayesian optimization, have been used to automate this process. During experiments on real-world systems such as robotic platforms these methods can evaluate unsafe parameters that lead to safety-critical system failures and can destroy the system. Recently, a safe Bayesian optimization algorithm, called SafeOpt, has been developed, which guarantees that the performance of the system never falls below a critical value; that is, safety is defined based on the performance function. However, coupling performance and safety is often not desirable in practice, since they are often opposing objectives. In this paper, we present a generalized algorithm that allows for multiple safety constraints separate from the objective. Given an initial set of safe parameters, the algorithm maximizes performance but only evaluates parameters that satisfy safety for all constraints with high probability. To this end, it carefully explores the parameter space by exploiting regularity assumptions in terms of a Gaussian process prior. Moreover, we show how context variables can be used to safely transfer knowledge to new situations and tasks. We provide a theoretical analysis and demonstrate that the proposed algorithm enables fast, automatic, and safe optimization of tuning parameters in experiments on a quadrotor vehicle.

Safety Analysis of a Certifiable Air Data System Based on Synthetic Sensors for Flow Angle Estimation

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.

A comparison of hazard analysis methods capability for safety requirements generation

A safety-critical system comprising several interacting and software-intensive systems must be carefully analyzed to detect whether new functional requirements are needed to ensure safety. This involves an analysis of the systemic properties of the system, which addresses the effect of the interaction between systems and system parts. The paper compares two hazard analysis methods, which are often considered well-suited for such software-intensive systems: the Functional Hazard Analysis (FHA) and Systems-Theoretic Process Analysis (STPA). The focus is on the selection and improvement of the best methods, based on the lesson learned from the comparison of FHA and STPA. The analyses cover the hazard analysis processes, systemic properties, and the criteria of requirements. The paper concludes that STPA is the better choice over FHA. Insights are obtained to align both STPA and FHA methods with the broader topic on risk management, that is, hazard analysis method improvement, cautionary thinking, uncertainty management, and resilience management.

Modeling and verification of train departure scenario for next generation train control system

As a complex and safety-critical system, any failure in the Next Generation Train Control System (NGTC) departure scenario may cause serious personal injuries and property losses. It is very necessary to study NGTC scenario scheme and effective modeling and verification methods. This paper investigates the key technologies of the NGTC, optimizes the system structure and redistribution functions, and proposes the train control system scheme and typical operating scenarios. Firstly, the structure, equipment function and information interaction of NGTC are analyzed, and the operation scenarios of the system scheme are designed. This paper also uses UML language to describe the train departure scenario, and uses NuSMV modeling to verify accessibility and certainty of the scenario scheme. The results show that, the scheme proposed in this paper provides a reference for the design and implementation of the NGTC.