Requirements and Safety Analysis using Constraints - CoRSA 

Kevin J. Hollingworth 1 
Centre for Software Reliability
University of Newcastle upon Tyne

Effective approaches for the safety analysis of large-scale embedded systems are urgently needed. Approaches based on safety engineering , software development and formal notations have been proposed, however these suffer from a number of deficiencies.  Motivation for a constraint-based approach is provided by related work on confirmation of consistency and verification of modelling notations for hardware and control systems. 

CoRSA provides an approach for safety analysis of requirements specifications and is amenable to automation. CoRSA establishes a relationship between the analysis of safety properties of a state transition model [Manna 95] and the resolution of a series of constraint satisfaction problems (CSPs). CoRSA realises the following benefits: 

  • Earlier safety analysis. Establishing safety criteria for, and limiting the propagation of critical errors to, subsequent development. 
  • Analysis of heterogeneous systems. Enable the effects of interaction between components, of different technologies, to be determined. 
  • Exploration of failure behaviours. Providing flexible and simple methods to explore failure behaviours and fault tolerant strategies.
  • Efficient analysis procedures. Partitions the safety analysis process into several analysis steps, each of which can be solved automatically.

CoRSA provides a number of views over a state transition system;  a template notation, a textual language and a constraint-based language (CBL). Extracts of the CoRSA views can be found in figure below. 

  • Template notation. A CoRSA template is an abstraction of a state transition system where the state space is created from a number of variables describing the system. The behaviour of the system and hazards are represented as a number of constraints over the current state and or successor states of the variables. Failure behaviours can be represented in a template, allowing faults to be injected into the system model. The template notation aids the analyst in modelling and analysis is supported by translation of a completed template , via mappings defined in the textual language, into a series of CSPs. 
  • Textual language. The textual language consists of a basic language and a macro language. The basic language  maps the templates to a CBL and encodes the analysis checks, in terms of three basic constraints: initial, invariant and transition. Analysis checks describe analysis procedures for transition systems as a CSP.  The macro language supports the definition of high level constraints, a call to a macro is expanded into a set of constraints expressed in terms of the basic language.  Macros have been developed for expression of timing requirements, in terms of delays and deadlines, and are currently being explored for an object oriented version of CoRSA. 
  • Constraint based language. The CBL is used to implement a number of CSPs , produced by the textual language, and to solve those problems. The CBL  used is OZ [OZ] . The textual language produces a generic set of CSPs, hence any CBL may be used. An analysis check succeeds if no solution is found (similar to proof by contradiction); for each failed check a pair of current and successor states leading to the violation are identified.  These can be used to reason about the defects in templates, supporting rectification.

The activities of CoRSA start with the external and elicitation activities and progress through to analysis. 

  • External Activities.  Produce a set of hazard definitions through a preliminary hazard analysis of the top-level requirements. 
  • Elicitation Activities.  Modelling the top-level requirements in terms of a CoRSA template and establishing validation conjectures. Checks are defined and conducted to confirm consistency and validate the CoRSA model.
  • Expression Activities. Encoding the hazards and failure behaviours in the template notation. CSPs are then produced, using the textual language, to define both normal and failure safety analysis checks.
  • Analysis.  Analysis is performed through the resolution of the CSPs produced by the expression activities. 

CoRSA has been applied to the gas burner benchmark example [Ravn 93],  this example has been used by other research to demonstrate software safety analysis techniques, those based on  FTA and HAZOPS. In our work, we extend the gas burner  by including some redundant components, in order to explore safety analysis for a simple fault tolerant system. 

An object-oriented version of CoRSA is under development, this will be applied to an industrial strength case study based on a fuel management system. The objective is to model the fuel transfer function, analyse system properties and establish a role for CoRSA in the context of current industrial development and assessment practices. This will be a joint effort between the CSR at Newcastle University and BAe Airbus. 

References

[Manna 95] Z.Manna and A.Pneuli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995. 
[OZ] OZ Web Site, Programming Systems Lab,  Department of Computer Science, Universität des Saarlandes German Research Centre for Artificial Intelligence, DFKI GmbH  Sonderforschungsbereich 378. URL http://www.ps.uni-sb.de. 
[Ravn 93]A.P.Ravn, H.Rischel and K.M.Hansen.  Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, SE-19(1):41-55, January 1993.

1. Author contact: Centre for Software Reliability, Bedson building, University of Newcastle, Newcastle upon Tyne, NE1 7RU, UK.Phone: +44 191 222 5042. Fax: +44 191 222 8788. E-Mail: K.J.Hollingworth@ncl.ac.uk.