Adaptive Integrated Formal Design of Safety-Critical Systems (Academy of Finland)

The main objective of the project ADVICeS is to develop a collection of tactics for system modelling that is based on formal methods. The aim is to make the formal design process more efficient, flexible and maintainable for developing complex, dependable software systems that are correct by construction. A combination of an adaptive design framework with formal methods is meant to augment the development flexibility and give faster response to changes and, hence, will aid to achieve a feasible formal development process that enhances maintainability. Integrating metrics and quality measurements with the formal design will provide additional development guidelines to support the modelling and enable the assessment of the suitability of the proposed hybrid method.

The main goals of the project ADVICeS (Adaptive Integrated Formal Design of Safety-Critical Systems) was to create tactics, like visualizations, patterns and integrated quality measurements, for the formal design in order to achieve a flexible and efficient design method for safety-critical systems. The result of our research in the project is the framework FormAgi where formal and agile development methods are combined to guarantee the correctness of the system while the development is performed as a flexible team work in a cost-effective way. By using libraries of graphically represented components, as well as development patterns and strategies, we can further facilitate the development of these safety-critical systems. Moreover, we have developed metrics to be able to monitor and guarantee the quality of the systems. To encourage the use of our hybrid design process we have created guidelines for practitioners of different levels of expertise.

The key methods within the ADVICeS project is the FormAgi framework combining formal and agile development methods employing a component-based reuse strategy for the Event-B method improving reuse of Event-B artefacts via a library of components. Metrics were established for evaluating and validating this merged development process. Moreover, to facilitate the use of this hybrid design method guidelines were created for practitioners of different levels of expertise. We experienced industrial interest in our work by Thales Austria GmbH (AT) and Vaadin (FI).