Parallel Development of Event-B Systems with Agile Methods

Formal methods have been used for some decades in safety critical systems such as software for transport systems. Therefore, formal development is needed in industry, nowadays even to a greater extent, especially in combination with tailored software engineering practices. Due to industrial needs, software engineering practices of today embrace agile principles of flexibility and adaptability. The development process should preferably be iterative and performed by a team. At each iteration step the team should have developed working software. Moreover, the requirements of the system might change over time, thus the development process should be responsive to these changes. Communication within the team and to the outside world is vital for the successful progress of the development. In this paper, we are interested in an agile approach to developing formal models. The stepwise nature of the formal development process matches the agile principles very well. Moreover, visualisation and animation of the formal development is essential for an agile approach, as it allows the team members to communicate their different aspects of the system effectively. However, the development in teams also requires parallel development of models which is fundamental in the agile approach. In parallel development the model is usually decomposed into subparts. However, this demands a substantial initial development as a single chain and still has the disadvantage of not supporting multiple abstractions. Here we are investigating an alternative approach which starts modelling from several different abstractions independently and subsequently merges the developments to approach a single refined model of the complete system.