Software fault trees and weakest preconditions: a comparison and analysis

Software development in safety-critical systems demands techniques which provide both the precision of formal methods and the practicality of tried and trusted engineering methods, giving a measure of rigour as required by the application. In particular, reasoning about system behaviour in the presence of failures requires a realistic use of formal methods. The authors show how to capture the semantics implied by software fault trees using a form of weakest precondition programming in modelling the failure properties of different software expressions as an example. They propose a traditional view in the application of fault trees to software expressions, which leads to a difference in their expression in weakest precondition semantics