Cited By
View all- Binamungu LMaro S(2023)Behaviour driven developmentJournal of Systems and Software10.1016/j.jss.2023.111749203:COnline publication date: 13-Jul-2023
Legislation-driven development of a Gift Aid system using Event-B
Authors: 
David M. Williams, Salaheddin Darwish, Steve Schneider, David R. MichaelAuthors Info & Claims
Pages 251 - 273
Abstract
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.
References
References
[1]
Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, and Voisin L Rodin: an open toolset for modelling and reasoning in Event-B Int J Softw Tools Technol Transf 2010 12 6 447-466
[2]
Abrial J-R The B-book: assigning programs to meanings 1996 Cambridge Cambridge University Press
[3]
Abrial J-R Modeling in EventB: system and software engineering 2010 Cambridge Cambridge University Press
[4]
Behave: behavior-driven development, python style. https://github.com/behave/behave. Accessed 24 May 2019
[5]
Carter J (2017) BHive: behaviour-driven development meets B-method. Ph.D. thesis, The University of Guelph
[6]
Common criteria for information technology security evaluation. V3.1r5. Technical report, Common Criteria (2017)
[7]
Cucumber: 10 minute tutorial. https://cucumber.io/docs/guides/10-minute-tutorial/. Accessed 24 May 2019
[8]
Cucumber: a tool that supports behaviour-driven development. https://github.com/cucumber/cucumber. Accessed 24 May 2019
[9]
Falampin J, Le-Dang H, Leuschel M, Mokrani M, and Plagge D Improving railway data validation with ProB 2013 Berlin Springer 27-43
[10]
Gherkin Reference: Cucumber. Accessed 24 May 2019
[11]
Gmehlich R and Jones C Experience of deployment in the automotive industry 2013 Berlin Springer 13-26
[12]
Hallerstede S, Leuschel M, and Plagge D Validation of formal models by refinement animation Sci Comput Program 2013 78 3 272-292
[13]
HMRC (2016) The donations to charity (gift aid declarations) regulations 2016. Statutory instruments
[14]
HMRC (2018a) Alternative method of VAT collection—split payment. Summary of responses
[15]
HMR (2018b) Charitable giving and gift aid. HMRC research report 482
[16]
HMRC (2018c) Measuring tax gaps 2018 edition. An official statistics release
[17]
Hoare CAR An axiomatic basis for computer programming Commun. ACM 1969 12 10 576-580
[18]
Hansen D, Schneider D, Leuschel M (2016) Using B and ProB for data validation projects. In: Proceedings ABZ 2016, pp 167–182. Springer International Publishing
[19]
Hoang TS, Schneider S, Treharne H, and Williams DM Foundations for using linear temporal logic in Event-B refinement Formal Asp Comput 2016 28 6 909-935
[20]
Ilić D, Laibinis L, Latvala T, Troubitsyna E, and Varpaaniemi K Deployment in the space sector 2013 Berlin Springer 45-62
[21]
JBehave: a framework for behaviour-driven development. https://jbehave.org/. Accessed 24 May 2019
[22]
Leuschel M and Butler M ProB: A model checker for B FME 2003: formal methods 2003 Berlin Springer 855-874
[23]
Larsen PG, Fitzgerald JS, Wolff S (2010) Are formal methods ready for agility? a reality check. Technical report no. CS-TR-1218, Newcastle University
[24]
Ladenberger L, Leuschel M (2016) BMotionWeb: A tool for rapid creation of formal prototypes. In: Software engineering and formal methods—14th international conference, SEFM 2016, Held as part of STAF 2016, Vienna, Austria, July 4–8, 2016, Proceedings, pp 403–417
[25]
Manifesto for agile software development. https://agilemanifesto.org/. Accessed 24 May 2019
[26]
Principles behind the agile manifesto. https://agilemanifesto.org/principles.html. Accessed 24 May 2019
[27]
North D (2006) Introducing behaviour-driven development (BDD). Better Software
[28]
Romanovsky A and Thomas M Industrial deployment of system engineering methods providing high dependability and productivity 2013 Berlin Springer
[29]
Siqueira FL, de Sousa TC, Silva PSM (2017) Using BDD and SBVR to refine business goals into an Event-B model: a research idea. In: 2017 IEEE/ACM 5th international FME workshop on formal methods in software engineering (FormaliSE), pp 31–36. IEEE
[30]
Snook C, Hoang TS, Dghyam D, Butler M, Fischer T, Schlick R, Wang K (2018) Behaviour-driven formal model development. In: Formal methods and software engineering, pp 21–36. Springer
[31]
Smart JF (2015) BDD in action: behavior-driven development for the whole software lifecycle. Manning
[32]
Streeva. Swiftaid. https://swiftaid.co.uk/. Accessed 09 July 2019
[33]
Schneider S, Treharne H, and Wehrheim H The behavioural semantics of Event-B refinement Formal Asp Comput 2014 26 2 251-280
[34]
Solis C, Wang X (2011) A study of the characteristics of behaviour driven development. In: 2011 37th EUROMICRO conference on software engineering and advanced applications, pp 383–387. IEEE
[35]
UKRI gateway to research: Swift Aid project reference 133294. https://gtr.ukri.org/projects?ref=133294. Accessed 24 May 2019
[36]
Woodcock J and Davies J Using Z: specification, refinement, and proof 1996 Upper Saddle River Prentice Hall
[37]
Williams DM, Darwish S, Schneider S, and Michael DR Swiftaid rodin event-b models Zonodo 2020
[38]
Wieczorek S, Kozyura V, Wei W, Roth A, and Stefanescu A Business information sector 2013 Berlin Springer 63-79
[39]
Werth M, Leuschel M (2020) VisB: A lightweight tool to visualize formal models with SVG graphics. In: Proceedings ABZ 2020, LNCS
Recommendations
Towards the Composition of Specifications in Event-B
The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
Formal goal-oriented development of resilient MAS in event-b
Ada-Europe'12: Proceedings of the 17th Ada-Europe international conference on Reliable Software TechnologiesGoal-Oriented Development facilitates structuring complex requirements. To ensure resilience the designers should guarantee that the system achieves its goals despite changes, e.g., caused by failures of system components. In this paper we propose a ...
DevOps meets formal modelling in high-criticality complex systems
QUDOS 2015: Proceedings of the 1st International Workshop on Quality-Aware DevOpsQuality is the cornerstone of high criticality systems, since in case of failure not only major financial losses are at stake, but also human lives. Formal methods that support model based-development are one of the methodologies used to achieve ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s) 2020.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 July 2020
Accepted: 09 April 2020
Received: 16 October 2019
Published in FAC Volume 32, Issue 2-3
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 80Total Downloads
- Downloads (Last 12 months)33
- Downloads (Last 6 weeks)6
Reflects downloads up to 03 Jan 2025
Other Metrics
Citations
Cited By
View all- Binamungu LMaro S(2023)Behaviour driven developmentJournal of Systems and Software10.1016/j.jss.2023.111749203:COnline publication date: 13-Jul-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in