Legislation-driven development of a Gift Aid system using Event-B

David Williams, Salaheddin Darwish, Steve Schneider, David R. Michael

Research output: Contribution to journalArticlepeer-review

178 Downloads (Pure)


This work presents our approach to formally model the Swiftaid system design, a digital platform that enables donors to automatically add Gift Aid to donations made via card payments. Following principles of Behaviour-Driven Development, we use Gherkin to capture requirements specified in legislation, specifically the UK Charity (Gift Aid Declarations) Regulations 2016. The Gherkin scenarios provide a basis for subsequent formal modelling and analysis using Event-B, Rodin and ProB. Interactive model simulations assist communication between domain experts, software architects and other stakeholders during requirements capture and system design, enabling the emergent system behaviour to be validated. Our approach was employed within the development of the real Swiftaid product, launched by Streeva in February 2019. Our analysis helped conclude that there was not a strong enough business case for one of the features, whichwas shown to provide nominal user convenience at the expense of increased complexity. This work provides a case study in allying formal and agile software development to enable rapid development of robust software.
Original languageEnglish
JournalFormal Aspects of Computing
Early online date25 May 2020
Publication statusEarly online - 25 May 2020


Dive into the research topics of 'Legislation-driven development of a Gift Aid system using Event-B'. Together they form a unique fingerprint.

Cite this