ABSTRACT

There is an important benefit of using formal methods in requirements engineering and elsewhere. Formal methods represent a universal language with very strict rules. Formal methods involve mathematical techniques. Formal methods have been in use by software engineers for quite some time. The Backus-Naur (or Backus-Normal) Form (BNF) is a mathematical specification language originally used to describe the Algol programming language in 1959. Category theory (CT) permits functional notation to be used to model abstract objects and is therefore useful in formal specification of those objects. Consistency checking using Boolean satisfiability is a powerful tool. Theorem proving techniques can be used to demonstrate that specifications are correct. A system is correct if it produces the correct output for every possible input, and if it terminates. Hoare logic features straightforward mathematical notation and proof techniques. Given a formal specification, a model checker can automatically verify that certain properties are theorems of the specification.