Validation methods using formal techniques - Probert, P; Lamb, D (Publ by IEE, 1991)
For many years computer scientists have been developing languages and techniques to clarify the structure of programs through establishing a sound mathematical foundation. The techniques included under the general umberella of formal methods have been introduced especially to put the design phase of program onto an analytical basis. Through demanding a precise mathematical notation at each stage of specification and design, they enforce a clarity of thought as well as providing methods for mathematically verifying that a program meets its specification. These methods have been applied very successfully for specification in areas ranging from databases to microprocessors. In this paper we examine their applicability in verifying and validating control software.