Agile Development of Formal Systems Models

Colin Snook, Marina Walden, Andrew Edmunds, Michael Butler

Research output: Book/Journal/ReportCommissioned reportProfessional

61 Downloads (Pure)


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.
Original languageEnglish
PublisherTurku Center for Computer Science (TUCS)
ISBN (Print)978-952-12-3792-8
Publication statusPublished - 2019
MoE publication typeD4 Published development or research report or study

Publication series

NameTUCS Technical Report


  • team-based
  • agile methods
  • formal methods
  • refinement
  • iUML-B
  • Event-B


Dive into the research topics of 'Agile Development of Formal Systems Models'. Together they form a unique fingerprint.

Cite this