The Unit-B Method — Refinement Guided by Progress Concerns (Abstract)

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 proper- ties. 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 ex- ample to show that systems development can be driven by not only safety but also liveness requirements.

Keywords: progress properties, refinement, fairness, scheduling, Unit-B, proof-based formal methods, verification of cyber-physical systems.