Agile Development of Formal Systems Models

Colin Snook, Marina Walden, Andrew Edmunds, Michael Butler

Forskningsoutput: Bok/tidskrift/rapportBeställd rapportProfessionell

33 Nedladdningar (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.
FörlagTurku Center for Computer Science (TUCS)
ISBN (tryckt)978-952-12-3792-8
StatusPublicerad - 2019
MoE-publikationstypD4 Publicerad utvecklings- eller forskningsrapport eller studie


NamnTUCS Technical Report


Fördjupa i forskningsämnen för ”Agile Development of Formal Systems Models”. Tillsammans bildar de ett unikt fingeravtryck.

Citera det här