Validating Formal Verification Using Safety Analysis Techniques

摘要

The increased interest in the use of automated safety analysis is supported by211u001ethe claim that manual safety analysis based on traditional techniques is error-211u001eprone, costly and not necessarily complete. It is also claimed that traditional 211u001etechniques are not able to deal with the inherent complexities of software 211u001eintensive systems. However, the authors show in this paper that a transition 211u001e(from manual to automatic approaches) in the assessment process and technologies 211u001eis accompanied by an inherent risk of obtaining false confidence, unless 211u001esafeguards are provided. The safeguard presented in this paper integrates 211u001etraditional deductive and inductive analysis techniques with model checking, a 211u001eform of formal verification. The aim is to provide a safety analyst with a 211u001erigorous approach for the validation of formal models. The feasibility of the 211u001eoverall approach is illustrated in terms of a case study.