The term "formal methods" refers to the use of (mainly) logical formalisms in the pursuit of improved software and hardware, including reliability, security, safety, productivity and reuse. Particular thrusts include code verification, design verification, generating programs from specifications, and generating test cases from specifications. A fairly comprehsnsive (though Eurocentric) overview of methods and groups can be found in the Oxford Formal Methods Archive.
Good engineering practice should be part of every system development effort, but it is amazing how poor the state of practice is for software, compared to the state of the art. Among often ignored basic Software Engineering Principles are the following:
Code verification is a classical subject, but is of doubtful practical value except in very critical cases; design verification is more promising. However, code verification can have pedagogical value. Much of the early work in formal methods was motivated by security, especially operating sytems for national security applications, but perhaps the most prominent applications today concern hardware, due to the extremely high cost of errors in the design of commercial microprocessors. The most prominent method in this area is model checking, mainly because it requires little sophistication on the part of its users.
Another very active area is computer-supported theorem proving; there are many projects, at many sites around the world, with many application areas, just a few of which are smart cards, the Java abstract machine, communication protocols, automotive software, hardware arithmetic, nuclear reactor software, secure message systems, and software for NASA spacecraft. Progress in this area has been fueled by dramatic increases in computer power, as well as by gradual improvements in the underlying theories and technologies, and the gradual accumulation of experience with increasingly complex problems.
Perhaps the most widely used theorem proving system today is HOL (an abbreviation for higher order logic), from Mike Gordon's Automated Reasoning Group at Cambridge University; another popular system is PVS, from the group headed by John Rushby at SRI International. HOL is essentially a proof checker for higher order logic, while PVS is especially noted for the rich collection of decision procedures that it integrates. The Cambridge group has been largely concerned with hardware, while the SRI group has been somewhat focused on security. Many other groups are concerned with theorem proving technology itself and/or with applications to mathematics, rather than with practical applications, and a huge diversity of logics are in common use.
A recent trend in the formal methods community, sometimes called lite formal methods, or light weight formal methods, aims to use formal methods in ways that are minimally disruptive to actual system development practice in particular contexts. Some Aspects of Lite Formal Methods are the following:
| BACK | NEXT |