The Unit-B Method -- Refinement Guided by Progress Concerns

TL;DR

The paper introduces Unit-B, a formal method for stepwise software system design that incorporates progress concerns through novel scheduling notions, enabling reasoning about both safety and liveness properties.

Contribution

It presents a new refinement method with coarse and fine schedules, generalizing fairness notions, and proof rules for progress properties, demonstrated through an illustrative example.

Findings

Unit-B effectively integrates safety and liveness reasoning.

The method's proof rules facilitate progress verification.

An example shows practical applicability of the approach.

Abstract

We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events' scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.