Description

Insurmountable complexity and a staggering amount of legacy is driving large companies to search for alternative ways of managing their codebases [2] [3] [4]. ING are a prime example who are researching if model-driven engineering is their holy grail. Their plan is to create a Domain-Specific Language (DSL) called Rebel [4] to specify their business logic and to generate the entire code base from these DSL specifications. Given that the code generator is verified, any changes to the code should not lead to any programming issues. Business logic issues still remain and our task is to find useful properties to verify and techniques to prove these properties. Finding and/or proving properties such as safety properties and no deadlocks narrows the type of bugs that can occur even further.

Rebel specifications use a Symbolic Transition System (STS) at its core. These variations of state machines describe the states and executions of a program. A node in the system corresponds with a state and a transition corresponds with one ”step” in the program. Modifications are described through first-order logic constraints on each transition. The goal our research is to find and describe useful properties to verify and to create and prototype a verification procedure to verify these useful properties. In our approach we combine a constraint-gathering principle[1] with k-induction[5] to find all possible states in all nodes after which we can use a SMT solver to verify any desired properties.

[1] Kai Bakker. Reachable States for Symbolic Transition Systems. PhD thesis, University of Amsterdam, 2015.

[2] Julian Huijbregts. Tax Authority concludes that the collection of taxes is in jeopardy due to IT-issues., 2017.

[3] Jan Ouwens. Mortgage DSL at the Rabobank, 2016.

[4] Jouke Stoel, Tijs Van Der Storm, Jurgen Vinju, and Joost Bosman. Solving the Bank with Rebel. 3(ITSLE 2016):13–20, 2016.

[5] Thomas Wahl. The k-Induction Principle. (including 0):1–2, 2013.

Additional Resources

1. The paper