A case study in software safety assurance using formal methods

Atchison, Brenton, Lindsay, Peter and Tombs, David (1999) A case study in software safety assurance using formal methods. SVRC Technical Report 99-31, Software Verification Research Centre, School of Information Technology, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
Author Atchison, Brenton
Lindsay, Peter
Tombs, David
Title A case study in software safety assurance using formal methods
School, Department or Centre Software Verification Research Centre, School of Information Technology
Institution The University of Queensland
Report Number 99-31
Series SVRC Technical Report
Publication date 1999-09
Total pages 66
Publisher SVRC
Language eng
Formatted Abstract/Summary This report describes a formal approach to verification and validation of safety requirements for embedded software, by application to a simple control-logic case study. The logic is formally specified in Z. System safety properties are formalised by defining an abstract model of the system’s physical behaviour in Z, including its hazardous states and dominant sensor failures. The Possum specification-animation tool is then used to check that the logic meets its safety requirements. Finally, the logic is implemented in SPARK Ada and SPARK Examiner is used to formally verify the implementation meets its specification. Design safety validation and source code verification are completely automated, removing the need for human intervention.
Keyword Safety critical systems
Formal methods
Safety assurance
Q-Index Code AX
Q-Index Status Provisional Code
Institutional Status UQ

Document type: Department Technical Report
Collection: School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 19 Abstract Views, 1 File Downloads  -  Detailed Statistics
Created: Mon, 05 Nov 2012, 15:23:19 EST by Dr. Nisansala Yatapanage on behalf of School of Information Technol and Elec Engineering