Agile Development of Formal Systems Models

Agile development methods are essential for developing large cyber-physical systems. These systems are often safety- or security-critical requiring rigorous verification. Formal model-driven methods with verification by theorem provers offer strong assurance of critical properties but do not fit easily with team based development. We propose a modelling process that draws on agile techniques and structures the development into parallel refinement paths that can be allocated to coordinated independent teams. Our approach is based on multiple abstractions germinating from critical properties and refined in parallel using a common dictionary of data and events to maintain consistency. A library of model fragments,one per requirement, is assembled in a preliminary phase. The model fragments are then added into each refinement path so that the parallel developments converge to a common model that is proven to satisfy all of the critical properties.The model development process is systematic allowing a low-risk engineering solution reducing reliance on highly skilled formal methods experts. We illustrate our method with a railway case study.