Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Using formally defined design patterns to improve system developments

  • Speaker:   Prof  Jean-Raymond Abrial  (ETH Zurich)
  • Host:   Richard Banach
  • 22nd November 2006 at 14:15 in 1.5
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
▲ Up to the top