The integration of safety analysis and functional verification techniques for software safety arguments

Atchison, Brenton (2004). The integration of safety analysis and functional verification techniques for software safety arguments PhD Thesis, School of Information Technology and Electrical Engineering, The University of Queensland.

       
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
THE17659.pdf Full text application/pdf 11.73MB 3
Author Atchison, Brenton
Thesis Title The integration of safety analysis and functional verification techniques for software safety arguments
School, Centre or Institute School of Information Technology and Electrical Engineering
Institution The University of Queensland
Publication date 2004
Thesis type PhD Thesis
Supervisor Prof Peter Lindsay
Prof Paul Strooper
Total pages 209
Language eng
Subjects L
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Formatted abstract As software-based systems gain increased responsibility for the control of safety-critical applications, regulatory and certification authorities are requiring higher assurance that such systems are acceptably safe for operation. A feature of this trend is the increased requirement to address software in system safety cases justifying the safety of systems deployed for service.

This thesis is concerned with a key part of the safety case, the analytical safety argument, which verifies the transformation of safety requirements from operational concept through levels of system design to software implementation. In particular, it examines the role of two different methodologies used in analytical safety arguments: safety analysis and funnctional verification. Safety analysis traditionally provides the core of a safety engineering program and is directed towards establishing that the risk of harm arising from system operation is acceptably low. Functional verification is a key process of software engineering and is directed towards eliminating or detecting errors with respect to a specification.

Safety arguments for software-intensive systems require the use of both safety analysis and V&V. However, since safety analysis and V&V techniques ha\e originated from different disciplines, there are different opinions about how they should be applied. Various strategies are embodied in the requirements of industry standards but there is almost no recognition that alternative strategies are possible and no studies to investigate the merits of different approaches.

The hypothesis of this thesis is that standards and guidelines should allow difTerent strategies for constructing analytical safety arguments that vary the division of responsibility between safety analysis and functional verification. This is established by constructing two alternative, equally sound, safety arguments, which integrate safety analysis and functional verification at different levels of design.
The two arguments are constructed for the same embedded control system, and address the analysis and design phases from system operational concept definition through to software implementation.

Both safety arguments begin with a Preliminary Hazard Analysis to identify overall system hazards and associated system safety requirements. Rigorous reasoning is applied to justify that the system safety requirements, together with some environmental assumptions, will prevent operational mishaps.
The remainder of the first argument uses functional verification and validation techniques without applying further safety analysis or distinguishing separate software safety requirements. Safety validation of a software functional specification is performed using specification animation. The software specification, expressed in a variant of Z, is systematically animated concurrently with a model of the equipment under control to identify reachable hazardous equipment states. The software specification is then refined to SPARK Ada source code that is then verified for correctness using the SPARK Examiner tool.

The second safety argument applies deeper safety analysis to identify specific software safety requirements and source code safety constraints. Safety requirements are expressed in temporal logic and the safety analysis is verified using rigorous proof. The software is implemented in SPARK Ada and the safety constraints are verified using SPARK Examiner.

The effectiveness of the two safety arguments is compared for the selected case study and issues of wider application are discussed, such as the scalability of results and the impact of safety assurance activities on the wider engineering process. While there are no general conclusions about the best safety argument strategy, the thesis demonstrates that the definition and use of standards and guidelines should be broadened to enable stakeholders the freedom to select the best approach to suit their application.
Keyword Computer software -- Verification
Computer software -- Reliability
System safety

 
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 104 Abstract Views, 3 File Downloads  -  Detailed Statistics
Created: Fri, 24 Aug 2007, 18:25:39 EST