Abstract Safety analysis can be labour intensive and error prone for system designers. Moreover, even a relatively minor change to a system’s design can necessitate a complete reworking of the system safety analysis. This paper proposes the use of Behavior Trees and model checking to automate Cut Set Analysis (CSA) : that is, the identification of combinations of component failures that can lead to hazardous system failures. We demonstrate an automated incremental approach to CSA, in which models are extended incrementally and previous results incorporated in such a way as to significantly reduce the time and effort required for the new analysis. The approach is demonstrated on a case study concerning the hydraulics systems for the Airbus A320 aircraft.

Abstract Failure Modes and Effects Analysis (FMEA) is a widely used system and software safety analysis technique that systematically identifies failure modes of system components and explores whether these failure modes might lead to potential hazards. In practice, FMEA is typically a labor‐intensive team‐based exercise, with little tool support. This article presents our experience with automating parts of the FMEA process, using a model checker to automate the search for system‐level consequences of component failures. The idea is to inject runtime faults into a model based on the system specification and check if the resulting model violates safety requirements, specified as temporal logical formulas. This enables the safety engineer to identify if a component failure, or combination of multiple failures, can lead to a specified hazard condition. If so, the model checker produces an example of the events leading up to the hazard occurrence which the analyst can use to identify the relevant failure propagation pathways and co‐effectors. The process is applied on three medium‐sized case studies modeled with Behavior Trees. Performance metrics for SAL model checking are presented. Copyright © 2011 John Wiley & Sons, Ltd.

Geoff Dromey's Behavior Engineering method provides a vital link between systems engineering processes and software engineering processes. It has proven particularly effective in industry when applied to large complex systems, to help understand the problem space and clarify system and software requirements. In this paper we compare the method with some of the most widely used system design methods, including State Transition Diagrams, Functional Flow Block Diagrams, Object Oriented Design, IDEF0, UML and SysML. The comparison draws on the Design-Methods Comparison Project undertaken by Bahill et al in 1998, and uses their Traffic Lights case study. We show that the methods are roughly equivalent in terms of what they can express, but that Behavior Trees come closest to natural language specification, which we contend makes them easier for non-formal methods experts to understand.

This paper demonstrates the use of Behavior Trees and model checking to assess system safety requirements for a system containing substantial redundancy. The case study concerns the hydraulics systems for the Airbus A320 aircraft, which are critical for aircraft control. The system design is supposed to be able to handle up to 3 different components failing individually, without loss of all hydraulic power. Verifying the logic of such designs is difficult for humans because of the sheer amount of detail and number of different cases that need to be considered. The paper demonstrates how model checking can yield insights into what combinations of component failures can lead to system failure.

Prioritisation is an important technique for resolving planning conflicts between agents with shared resources, such as robots moving through a shared space. This paper explores the use of genetic-based machine learning to assign priority dynamically, to improve performance of a team of agents without unduly impacting individual agents' performance. A decoupled heuristic approach is used for flexibility, whereby individual XCS agents learn to optimise their behaviour first, and then a high-level planner agent is introduced and trained to resolve conflicts by assigning priority. The approach is designed for Partially Observable Markov Decision Process (POMDP) environments and demonstrated on a problem in 3D aircraft path planning.

With the increased interest in multi-user systems with distributed decision making tasks, such as network centric warfare and free-flight air traffic control, the concept of shared situation awareness (SSA) has become more important. SSA relates to the awareness that different operators have of the system state and the information needs of their team-mates, in order to coordinate their actions effectively. However, there are many different definitions of SSA in the literature and no generally agreed methodology for measuring it. Investigation to date has primarily been conducted through human-in-the-loop (HIL) experiments, which typically are costly and return only subjective results. Agent based modelling has been proposed as a partial solution, using software agents to take the place of humans in experiments. This paper describes the application of agent based modelling to a multi-user system: namely, the SCUDhunt game. The paper examines different ways of sharing information between operators, and their effect on team performance in cases with less than perfect information. Agent based modelling enables performance to be tested on a wide range of scenarios quickly and repeatedly and yields insights that would be difficult to achieve through HIL experiments alone.

Free flight is a new concept in air traffic management, where pilots are given more freedom in making decisions in the cockpit. This allows air traffic controllers to manage more flights. One of the concepts under investigation in the Australian airspace is moving sectors, where an air traffic controller becomes responsible of a moving volume of the space containing a group of airplanes. Planning flight trajectories in this group is a hard problem. In this paper, we show that XCS can be used as a reliable planning tool. We also propose a novel idea for incorporating hard constraints within XCS to increase its reliability

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.

Software configuration management is the discipline of managing large collections of software development artefacts from which software products are built. Software configuration management tools typically deal with artefacts at fine levels of granularity - such as individual source code files - and assist with coordination of changes to such artefacts. This paper describes a lightweight tool, designed to be used on top of a traditional file-based configuration management system. The add-on tool support enables users to flexibly define new hierarchical views of product structure, independent of the underlying artefact-repository structure. The tool extracts configuration and change data with respect to the user-defined hierarchy, leading to improved visibility of how individual subsystems have changed. The approach yields a range of new capabilities for build managers, and verification and validation teams. The paper includes a description of our experience using the tool in an organization that builds large embedded software systems.

This paper describes a tool that manages a hierarchical, "is a subsystem of"-structure on a set of software development artefacts and that provides configuration management (CM) for subsystems by interacting with an existing CM tool. The tool is based on a recently proposed framework for subsystem-based configuration management. The tool demonstrates the feasibility of the framework and develops it further The design of the framework and the tool was developed in collaboration with Invensys SCADA Development and it is discussed in relation to their current software development process.

This paper reports on an industrial pilot project that introduces systematic, automated module testing for embedded software in distributed, real-time, control systems. The systems are used in safety-related applications, are complex in nature, and hence have strong requirements for test coverage, auditability and repeatability. This paper explores issues of isolating modules from the run-time environment, improving integration of testing into the development environment, automating testing, and improving test planning and documentation. Metrics were gathered throughout the project that allow a coarse cost-benefit evaluation. Code coverage metrics for statement and branch coverage were also gathered using a commercial code coverage analysis tool. The testing exposed a number of latent faults within the software, and the overall results of the project show that module testing is feasible for this complex, embedded software.

The CARE project investigated integration of well understood formal development principles into an industrial organisation's software development methodology. The result was a method for construction and verification of programs from formal specifications, using libraries of pre proven, formally specified components. Tools help the user build products by selecting and instantiating components to fit the problem at hand and generating and discharging correctness of fit proof obligations. The paper illustrates the method on part of the development of a software module for logging events in a medical embedded device.

Reports on a collaborative project to pilot the use of formal methods in the development of safety-related software. Using the SVRC's Cogito methodology, staff from CSC Australia undertook: formal specification; validation of the specification by mathematical consistency checks; hazard analysis; and validation of the specification against the safety requirements. Part of the design was modelled formally and verified.