Agile Development of Formal Systems Models

Colin Snook, Marina Walden, Andrew Edmunds, Michael Butler

Tutkimustuotos: Kirja/lehti/raporttiTutkimusraporttiAmmatillinen

33 Lataukset (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.
KustantajaTurku Center for Computer Science (TUCS)
ISBN (painettu)978-952-12-3792-8
TilaJulkaistu - 2019
OKM-julkaisutyyppiD4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset


NimiTUCS Technical Report


Sukella tutkimusaiheisiin 'Agile Development of Formal Systems Models'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.