Jouke stoel, PhD researcher at the Software Analysis and Transformation research group at Centrum Wiskunde & Informatica (CWI) developed new methods for the way large enterprises, like the ING bank, manage their intricate software systems. These innovative methods help clarify complex banking software, making it more reliable and secure.
In his thesis, titled "Solving the Bank: Lightweight Specification and Verification Techniques for Enterprise Software", Stoel delves into the application of Formal Methods, such as the B-method, VDM, and mCRL2, in enterprise software. Formal Methods involve specifying a system's behavior in a precise and formal notation, enabling automatic reasoning about properties like safety through theorem proving and model checking. However, the adoption of formal methods in large-scale industry projects has often been hindered by the perceived high cost in terms of time and expertise.
Enterprise software systems are large and complex systems consisting of many different sub systems. Keeping such a system in a consistent state while still extending and improving it, is a daunting task. Reasoning about the correctness of such a complex web of software systems is nearly impossible. Stoel describes the impact of different choices using lightweight formal methods, taking into account the partiality on the design and verification of enterprise software systems. In his research Stoel develops specification languages that allow users to be clearer and more precise in specifying the desired behavior of their systems. With these clear and precise descriptions, Stoel develops techniques for partial verification allowing users to formulate questions that are of interest to their domain. For instance, a bank employee can specify the intricacies of a saving account with these techniques and then formulate the questions whether this saving account could be overdrawn. A situation that is not allowed. By developing techniques that allow for bespoke compositions of these specifications a user is able to perform partial verification while still retaining the ability to specify the complete system.
This research, done in collaboration with the ING bank, a large Dutch national bank, is particularly relevant as the ING bank experiences similar challenges in their IT landscape. Their system has grown extensively over the past sixty years, containing numerous applications and sub-systems. Fully formalizing such a system would be a monumental task.
Jouke Stoel's research provides valuable insights into the application of lightweight specification and verification techniques in domains traditionally slow to adopt formal methods. The collaboration with the ING bank underscores the real-world applicability of these innovative approaches in addressing the challenges faced by the financial industry.
More information
- Jouke Stoel defended his thesis at Eindhoven University of Technology on Wednesday 6 November 2023. Promotors: Jurgen Vinju and Tijs van der Storm (Promotor), Mark van den Brand (Co-Promotor)
- Link to thesis
- Software Analysis & Transformation research group
