Open AccessA Generic Goal-Based Certification Argument for the Justification of Formal Analysis
Author(s) -
Ibrahim Habli,
Tim Kelly
Publication year - 2009
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2009.09.004
Subject(s) - certification , safety case , formal methods , computer science , argument (complex analysis) , software engineering , formal specification , refinement , trustworthiness , formal verification , certification and accreditation , risk analysis (engineering) , process management , computer security , programming language , engineering , business , political science , law , biochemistry , chemistry
Formal methods are powerful specification and verification techniques for establishing high confidence in safety-critical systems. However, there are a number of concerns about the use of evidence generated from formal methods, when used in place of conventional testing, for satisfying certain certification objectives. In this paper, we address this issue by reviewing two certification documents, DO-178B and the UK Defence Standard 00-56, focusing on their approach to accepting formal analytical evidence. We also present a generic goal-based safety case that can be instantiated to facilitate the justification and presentation of formal analysis to the certification authorities. The safety case is based on claims about (1) the achievement of the intents of the certification objectives, (2) the demonstration of the trustworthiness of formal analysis and (3) the practical feasibility of deploying formal methods within a specific project
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom