The Unit-B Method -- Refinement Guided by Progress Concerns
This work addresses the problem of ensuring both safety and liveness in software system design for developers and formal methods practitioners, representing an incremental advancement by building on Event-B and UNITY.
The authors tackled the challenge of designing software systems that satisfy both safety and liveness properties by introducing Unit-B, a formal method that uses coarse and fine schedules to generalize fairness assumptions and includes proof rules for progress properties, resulting in a refinement order that preserves these properties.
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.