Large organizations like banks suffer from the ever growing complexity of their systems. Evolving the software in the face of change 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. When domain knowledge is recorded it is captured in informal document (like Word files or Excel sheets) making it hard to relate the requirements to the actual implementation of the software. With Rebel we aim to capture, centralize and relate the domain knowledge 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. These specifications can be used as a method of communication between stakeholders, to check the existing system implementations and, ultimately, to serve as a base to generate new systems. Specifications can be translated into Satisfiability Modulo Theories (SMT) constraints, solved using an SMT solver, and translated back into the Rebel ISE for interpretation.

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.