Executable specifications in software reliability engineering
Bernhard K. Aichernig · 1999
mentions the use of formal methods for fault re-moval [9]: “When formal methods are in full swing, formal design proofs might be avail-able to achieve mathematical proof of correctness for programs. Also, fault-monitoring assertions could be employed through executable specifications, and test-cases could be automatically gener-ated to achieve efficient software verifica-tion.” In the following, so called light-weight applications of formal methods to Software Reliability Engi-neering (SRE) [10] are examined. ’Light-weight’ means that not correctness proofs are in the cen-