Prof. Dr. Stefan Hallerstede, University of Aarhus

Abstract:

Event-B is a formal modelling and verification method that is intended to be practical: to be used by practitioners (or, engineers) supported by an interactive software tool. Much of the appearance of Event-B originates in this objective.

One of the proof techniques that is to achieve the objective deals with termination. It permits to prove termination on lexicographical orders without spelling out the underlying order by "anticipating" termination of computations. The technique is applicable to sequential programs but most useful in the verification of concurrent programs.

We demonstrate its usefulness by way of two examples. By way of a third example we demonstrate that sometimes the technique complicates verification proofs. Worse, "sometimes" is often, in practice.

Now, in a practical method it appears necessary to decide at some point to adopt definitively the techniques to be supported. As a consequence, "work arounds" are developed for cases as the above. This also possible in our situation.

A far more satisfactory solution, however, is to keep the method and tool evolving and avoid developing "work arounds" whenever possible. We present a simple solution to the problem and sketch its proof of correctness.