How it works

For a successful integration of any two complex systems, one should consider all of their possible interactions. The problem is that for most “real-world” systems, especially in financial services, there may be virtually infinitely many such interactions. Luckily, recent advances in automated reasoning allow us to compress these state-spaces into finite number of symbolic regions and convert into test cases. One fundamental requirement to make this work is that specification should be expressed unambiguously. So we created a language called Imandra Protocol Language for encoding system interfaces with mathematical precision. Any such valid IPL model may be converted and analyzed by Imandra to automatically generate test cases.

IPL How it works diagram

IPL - Imandra Protocol Language

IPL is a formal (mathematically precise) language for specifying complex system interfaces as *infinite* state machines. An IPL model consists of the following elements: (1) State definition - global variable that maintains the state of the session; (2) Inbound message definition and handling logic - these are messages that a client system may send; (3) Action definitions and handling logic - these are internal system events which may cause the state to change and submit Outbound messages; and (4) Outbound message definitions and types - these are messages the model sends back.

IPL - Imandra Protocol Language

Exploring IPL model state spaces

Imandra’s Region Decomposition feature automatically analyzes IPL model’s state-spaces and compresses them into a finite number of symbolic traces, or sequences of state-transitions which we represent as graphs. Each graph starts with the initial state, and is followed by transitions to other states through symbolic actions. Each action represents either an inbound message or a system event, resulting in state change and some form of response. For each such transition, resulting state pair, Imandra produces a set of symbolic constraints describing precisely the event and its result.

Exploring IPL model state spaces

Automated test case generation

For each symbolic trace of the state-space, Imandra can generate source code to push the implementation into these state transitions and compare the resulting behavior with expectation. To make this happen, Imandra has powerful constraint solving features that analyze the symbolic traces and produce both, concrete values and synthesize source code. The output is highly customizable - we can generate printers for arbitrary languages and frameworks.

Example of test case source code
By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox