Formal Analysis and Verification of Accidents

This project aims to extend CAFAISHA, a cognitive architecture developed at NU, to incorporate STAMP, an accident causality model extensively used at ZHAW in industrial projects.

CAFAISHA (Cognitive Architecture for the Formal Analysis of Interactive Systems and Human Activities) consists of an arbitrary number of system components, interfaces and human components interacting through two distinct environments: an observable environment for the interaction between human components and interfaces, through human perceptions and actions, and a system environment for the interaction between system components and interfaces, through a communication network. System components may be modelled using various formal modelling languages, such as process algebras and Petri nets. Each human component is equipped with a model of short-term memory (STM) and a model of long-term memory (LTM). Human tasks are modelled as sets of rules describing basic human activities which are stored in LTM. Each rule is triggered by a perception, some information stored in STM and is executed by modifying the information in STM and possibly performing an action. In addition, rules describing deliberate behaviour are driven by goals, whereas rules describing automatic behaviour are not. The LTM also contains a representation of the mental model of the system with which the human interacts. CAFAISHA supports the continuous modification of both the rules describing human activities and the human expectations, driven by the feedback received and the experiences and new knowledge acquired during interaction. Properties of the interaction, expressed in temporal logic, can be verified using model checking.

STAMP (System-Theoretic Accident Model and Processes) is a framework that has been developed by Nancy Leveson (MIT) to model and analyse accidents. In STAMP, safety is viewed as a control problem and is managed by a control structure embedded in an adaptive socio-technical system and acting as constraints on the system. This project focuses on two controlling components of the system, the Human Supervisor and the Automated Controller. The Human Supervisor, in addition to having a mental model of the controlled process, also has a mental model of the automated controller behaviour. These two mental models evolve throughout the time and it is often their mismatch with the real process and the real controller to determine accidents. The Automated Controller has a model of the process and a model of the interface with which the human interacts. In many cases the automated controller does not directly issue control commands, but acts as an automated decision support providing information to the human controller. In such a situation, a possible lack of synchronisation between the human supervisor and the automated controller may lead to system accidents.

The project aims to extend CAFAISHA by

1) explicitly separating model of process and model of automation as distinct categories of system components;

2) defining and implementing the mechanisms for the evolution of the mental models for these two categories;

3) implementing a module for the high-level definition of safety constraints and their automatic translation into temporal logic;

4) implementing a module for the analysis of the counterexamples generated when model-checking safety constraints.

Participants:

Dr. Karl Lermer, Zurich University of Applied Sciences

Prof. Antonio Cerone, Nazarbayev University