Solving the bank with Rebel: on the design of the Rebel specification language and its application inside a bank
Large organizations like banks suffer from the ever growing complexity of their systems. Evolving the software becomes harder and harder since a single change can affect a much larger part of the system than predicted upfront. A large contributing factor to this problem is that the actual domain knowledge is often implicit, incomplete, or out of date, making it difficult to reason about the correct behavior of the system as a whole. With Rebel we aim to capture and centralize the domain knowledge and relate it to the running systems. Rebel is a formal specification language for controlling the intrinsic complexity of software for financial enterprise systems. In collaboration with ING, a large Dutch bank, we developed the Rebel specification language and an Integrated Specification Environment (ISE), currently offering automated simulation and checking of Rebel specifications using a Satisfiability Modulo Theories (SMT) solver. In this paper we report on our design choices for Rebel, the implementation and features of the ISE, and our initial observations on the application of Rebel inside the bank.
|DSL, Industry case, Language design, Model checking, SMT, Specification language|
|Industry Track on Software Language Engineering|
|This work was funded by the CWI PPS samenwerking; grant id pps/ - Adviseren en verrichten van onderzoek naar functionele en niet-functionele eigenschappen van een deel van ING's IT-infrastructuur|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam, The Netherlands|
Stoel, J, van der Storm, T, Vinju, J.J, & Bosman, J.W. (2016). Solving the bank with Rebel: on the design of the Rebel specification language and its application inside a bank. In ITSLE 2016 - Proceedings of the 1st Industry Track on Software Language Engineering, co-located with SPLASH 2016 (pp. 13–20). doi:10.1145/2998407.2998413