Navigation

Contact

EMail: scare@uol.fiaekde

DIRECTOR

Prof. Dr. Ernst-Rüdiger Olderog,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

oldeaduuroijg@inq8kveformaxz/tik+oxi.uni-oldey6nn0nburg.de

COODINATOR

Ira Wempe,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

irkmioa.wtlempe@inhnfo+wsrmatikx1i9p.unvqi-oldenbuzzccgrgez.deea

On Anticipating Termination in Event-B

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.

Oli0codver Th5beex9l (olirxg8ever.theel@uol.de) (Changed: 2020-01-23)