Imandra Protocol Language - VS Code Plugin

Imandra Protocol Language (IPL) is a formal (mathematically precise) language for modelling complex system interfaces as infinite state machines. Such representation allows for analysis by automated reasoning engines (such as Imandra) for model checking (correctness), automated test generation and simulation. For further information, check out:

IPL System Integration

For a 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 like financial services, 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. This opens tremendous opportunities to tap into AI for generating test cases, simulation environments and much more. The fundamental requirement to make this work is that specifications should be expressed unambiguously. We solve this with IPL - a language for encoding system interfaces with mathematical precision.

A specification expressed in IPL may be used to automatically:

Generate high-coverage (with explanations of behavior) test-cases
Audit production data to make sure it's in sync with the IPL model
Generate precise and correct documentation
Create simulation environments (DevOps)
Verify correctness properties
And much more...

IPL workflow

Modelling interfaces as infinite state machines

IPL models system interfaces as infinite state machines - these are powerful analogs to Finite State Machines (FSM) which are inadequate for "real world" systems. An IPL model consists of the following elements:

State definition - global variable that maintains the state of the session. It may have as many variables as you would like.
Inbound message definition and handling logic - these are messages that a client system may send to be processed by the model. For an Inbound Message to be valid, it must pass through "validity" statements which may be particular to a specific message field or combine multiple fields at once.
Action definitions and handling logic - these are internal system events which may cause the state to change and submit Outbound messages. Actions represent a powerful abstraction of how your system may respond to the inbound messages or other internal state events (e.g. time change). Just like with Inbound Messages, Actions are described with a set of type definitions, validity constraints and processing logic (e.g. which may emit Outbound Messages).
Outbound message definitions and types - these are messages that the model may send back. Their types are defined similarly to Inbound messages, but there are no validity checks as the logic to send them will always be in response to either an Inbound message or an Action.

IPL Model Outline

Note on Region Decomposition

One of IPL's special features is integration with Imandra's Region Decompositon (RD). RD is an automated technique for compressing algorithms' state spaces into finite number of symbolic regions. These regions completely describe the full functionality of the original algorithm - Imandra produces a mathematical proof of this. The output of this analysis may be transformed in English-prose descriptions, concrete test vectors, documentation or visualized as a graph of symbolic state changes (IPL Gallery has several examples of this).

Region Decomposition is inspired by Cylindrical Algebraic Decomposition, a fundamental technique for reasoning about nonlinear polynomial systems by decomposing Euclidean space into a finite number of connected regions s.t. within each region the behavior of the system under analysis is invariant. This effectively computes a “map” of all possible behaviors of the system, and facilitates a wide variety of nonlinear decision procedures over the reals and complexes. Imandra "lifts" CAD to algorithms at large, creating a fundamentally new technique for understanding systems' behavior and automatically generating high-coverage test suites.

Region Decomposition

IPL for Connectivity in Financial Services

IPL has a number of features specifcially for modelling financial trading system interfaces. For example, it has several versions of the FIX protocol as libraries. The current implementation supports the FIX versions 4.2, 4.4 and 5.0. Our roadmap also includes other widely used protocols such as SWIFT, FAST and ITCH.

For further information, please see Imandra Markets: Connectivity.