Software Engineering and Lite Formal Methods 1
Joseph A Goguen


  1. State of the art for formal methods in software engineering
  2. Lite formal methods
  3. BOBJ
  4. Kumo
  5. Hidden algebra
  6. Requirements Engineering
  7. Parameterized Programming and Software Architecture
  8. Institutions
  9. Data Integration
The first two of these are an essay on this webpage, while the rest appear on the next page, describing my personal interests.
1. State of the art for formal methods in software engineering

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:

It is often thought, e.g., by some advocates of so-called "extreme programming", that formal methods run contrary to all of the above, except possibly the last two. However, this is absolutely not the case, despite the fact that the practice and/or advice of many formal methods fanatics is often difficult or impossible to reconcile with current best practices in software engineering.

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.

2. Lite formal methods

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:

(The reader may compare this list with the Software Engineering Principles that appear earlier on this page.) My own research under this paradigm includes:
  1. Parameterized programming, for software modularization and reuse;
  2. Algebraic specification, particularly for designs of distributed concurrent systems; and
  3. Specification language design and implementation.
  4. Formal approaches to user interface design.
In addition, I have been concerned with the popularization of algebraic methods, especially category theory, and with some educational issues that arise. The next webpage discusses my research, under topics 3-9 of the above Table of Contents.

   BACK       NEXT   

Maintained by Joseph Goguen
Last modified: Sun Oct 28 20:42:37 PST 2001