For a long time, I have wanted to talk about discrete transition systems as the main abstraction of program execution. People use such abstractions for two reasons: producing theoretical results and reasoning about their programs. Although I don't have problems with the first one (I don't quarrel with people looking for theoretical results, I think it's a valid goal) I am looking to reason about my programs to document them with a proof of their correctness.
I always had a hard time to choose which part to start with and I think I got something nicely simple to talk of Event-B, UNITY and, my own creation, Unit-B. It focuses on the achievements of my master thesis but it should already make sense for anyone who is not my supervisor and who does not have any experience with any of the mentioned formal methods.
The goal of my master thesis was to design a formal method for developing correct parallel programs. The result is Unit-B, a formal method inspired Event-B and UNITY.
Using Unit-B, one can design a concurrent program by refining, step by step, a specification into a program in a similar fashion as in Event-B. However, while refinement in Event-B only preserves safety properties, refinement in Unit-B also preserves liveness properties. This means that, once it is established that a specification S satisfies a progress property P, all specifications and programs refining S will also satisfy P. It ensues that, as opposed to Event-B, it is possible in Unit-B to introduce progress properties in a specification along the refinement process exactly at the time where they make most sense rather than at the very end of a development.
The technique has two benefits. First, in Event-B, when one tries to establish a liveness property, it is often too late: while trying to make the system safe, one has removed any possibilities for the system to perform a useful function. Such is not the case with Unit-B. By tackling progress properties before the related safety properties, we eliminate the possibility of addressing safety concerns by being too conservative.
Second, by putting the requirement for progress as the center of attention in the process of refinement, the specification ends up shaping itself around the progress property. In other words, the concern for progress dictates the skeleton of a valid program. After that, the concern for safety can be seen as putting the flesh on the bones.
Compared to UNITY, this approach has the benefit of making the transition from specification to program smoother. Since a program is just a special kind of specification in Unit-B, the suitable application of refinement to specification will slowly give birth to a program. In UNITY, a specification and a program are two completely different things making the refinement of a specification and the creation of a program two distinct activities.
From UNITY, Unit-B takes the temporal logic and the fairness assumption in the execution of its transition system. Fairness facilitates the mapping between progress properties to transition systems and the temporal logic is tailored to express simply properties that can be mapped to programs.
The semantics of Unit-B is defined using the R.M. Dijkstra's computation calculus which allowed me to be very fine-grained in the choice of and in the proof of correctness of the refinement rules.
Cheers,
Simon Hudon
York U
Toronto, Canada
February 28th 2012
