Group colloquium: Static Analysis of Symbolic Transition Systems with Goose

When: Jan. 30, 2018, 12:30-13:30

Where: Hal B 2A

Who: Sebastiaan la Fleur

ING is working on a DSL called Rebel to be able to specify banking products from which code bases may be generated. The underlying formalism of Rebel is symbolic transition systems (STSs) which are directed graph structures with a set of state variables where each transition has a guard and a relation constraint. Transitions may be 'taken' for each state which is reachable in an origin node and which satisfies the guard. The relation specifies which states are reachable from the origin node to the destination node.

The main goal of our research is to find useful properties to verify for arbitrary STSs and an approach to verify these properties. We have found existing tools such as MCMT, nuXmv and Z3 (pdr) which are able to verify safety properties for infinite state systems; a class of systems to which STSs belong. Mappings have been found to specify arbitrary STSs in nuXmv and Z3 but evaluation has shown that certain issues exist which are significant for the ING use case. This has led to the development of the algorithm nicknamed Goose to verify more than safety properties for STSs. This talk will give an overview of the issues with existing systems and how Goose solves these issues. We will also show initial results which show that Goose is suitable for the ING usecase.