Formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, designers can not only verify the system’s properties in a more thorough fashion (than they could via empirical testing) but also use mathematical proof as a complement to system testing so as to ensure correct behavior.
Formal methods adopt a three-step approach to modeling and evaluating systems. During formal specification, an engineer or designer rigorously defines a system using a modeling language—typically by using a formal, mathematical syntax and semantics that eliminate imprecision and ambiguity. This is similar to writing down system specifications, though not in plain English. From there, based on the specification, the engineers develop a set of theorems about the behavior of a system. These theorems are verified through mathematical proofs—to ensure that the system behavior is logically consistent and is, indeed, the desirable one. As this allows designers and engineers to discover flaws in usability even before the design gets implemented into code, it prevents costly errors from emerging in the later stages of development. Finally, once the model is specified and verified, implementation can begin via converting the specification into code.
Formal methods have many advantages: they help disambiguate system specifications and articulate implicit assumptions. They also expose flaws in system requirements, and their rigor enables a better understanding of the problem. Because they use a formal language, many colleagues can verify the specifications independently—thereby solving errors early on in the development process. However, formal methods cannot fully replace standard quality assurance methods. This is why they are just a complementary technique in system design.
