How it works
For successful integration of complex systems, it's important to consider all of their possible interactions. The problem is that for most "real-world" systems, especially in safety-critical industries (e.g., finance), there may be virtually infinitely many such interactions. Luckily, recent advances in automated reasoning allow us to compress these state-spaces into a finite number of symbolic regions and convert them 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 generate test cases automatically.
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.
Exploring IPL model state-spaces
Imandra's Region Decomposition feature automatically analyzes the IPL model's state-spaces and compresses them into a finite number of symbolic traces or state-transitions sequences that 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, Imandra produces a set of symbolic constraints describing precisely the event and its result.
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.