Using formally defined design patterns to improve system developments.

The concept of "design pattern" is well known in Object Oriented
Technology. The main idea is to have some sort of reproducible engineering
micro-design that the software designer can use in order to develop new
pieces of software. In this presentation, I try to borrow such OO ideas
and incorporate them within  the realm of formal methods.

First, I will proceed by  defining (and prove) two formal patterns, where
the second one happens to be a refinement of the first one. As a matter of
fact, one very often encounters such patterns in the development of
reactive systems, where several chains of reactions can take place between
an environment and a software controller, and vice-versa.

Second, the patterns are then used many times in the development of a
complete reactive system where several pieces of equipment interact with a
software controller. It results in a systematic construction made of six
refinements. The entire system is proved completely automatically.

The relationship between the formal design patterns and the formal
development of the problem at hand will be shown to correspond to a
certain form of refinement.
A demo will be shown.