Mark's Goals for Formal Methods

My long term goal for formal methods is to see them being used in a cost-effective fashion on the majority of typical software developments, rather than just on safety-critical or security-critical applications.

By Formal Methods, I mean high-level mathematical notations that can be analyzed by computer. I'm particularly interested in the model-oriented notations, such as Z, B, AsmL and JML (Java Modeling Language).

My main interest is in using such notations to specify software, and to make my own software development more efficient by using formal methods.

Here is what I believe are the keys to more successful use of formal methods. (These ideas are developed from my own experience, plus study of the viewpoints in the article "An Invitation to Formal Methods", in IEEE Computer, April 1996).

  1. Focus on finding errors.

    It is as easy to write an incorrect specification as it is to write an incorrect program, so the primary focus of formal methods should be on detecting errors in specifications, in programs, and in other artifacts. Here are some practical consequences of this primary focus:

  2. Powerful Tools

    The primary attraction of formal notation is that it can be machine analyzed. For wide-spread use, we ideally want tools that are:

How should we go about working towards meeting these goals?

I am involved in the BZ-TT (BZ Testing Tools) project, which applies this kind of philosophy to automatic model-based test generation. The resulting tools are being commercialised by the company Leirios Technologies (http://www.leirios.com).

PS. The above list is not meant to be exclusive. It is simply an approach that appeals to me as being interesting and likely to be fruitful. Some other researchers share these goals. Others prefer a longer-term approach based on interactive theorem proving.


This article is translated to Serbo-Croatian language by Jovana Milutinovich from Webhostinggeeks.com.

marku@cs.waikato.ac.nz
Last modified: Fri Nov 16 14:47:56 EST 2012