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 Product Page
• IPL Documentation
• IPL Gallery

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...

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:

1. State definition - global variable that maintains the state of the session. It may have as many variables as you would like.

2. 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.

3. 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).

4. 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.

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.

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.

Related resources

• IPL Product page
• IPL Documentation
• IPL Gallery page
• IPL Model examples
• Article: The Wolf, Goat and Cabbage Exchange
• Article: Machine Reasonable APIs and Regulations

VS Code IPL Plugin in action

VS Code IPL Plugin commands

The following commands are accesible under the category Ipl when the extension is running.

Generate Documentation

For a valid .ipl file, this will generate html documentation for the file in the local directory called GeneratedDoc and will also navigate the default browser to this html file.

Generate Normalised Single File

In a multi file development it is possible to create a single file representing all of the imported artifacts and logic of the topmost file and has no local imports.

Submit File for Analysis

Given a valid Ipl file with no local imports (see above section on generating a normalised single file), and an Imandra login, it is possible to submit the file for analysis and test case generation. Instructions on obtaining an Imandra login are given here. The default browser is opened at the location of the online analysis.

Generate OCaml AST

Given a valid Ipl file it is possible to generate an OCaml representation of the file for analysis. This uses the publicly available repository given here. This file is generated in a directory called iplAst in the local workspace.

Generate Inverse

Given a valid Ipl it is possible generate an "inverse" which makes a file in the local workspace with the suffix <FILE>_inverse.ipl where <FILE>.ipl is the file chosen. This represents a file with the polarity of messages reversed - so outbound message become inbound and vice-versa.

Generate Ipl From Logs

If the current file is a FIX log and named with .ipl extension (so that the extension is active), then the extension will produce a file called genIpl<VENUE>.ipl where <VENUE> is the name of the inferred exchange (for example) to which messages are being sent. This generated valid Ipl file represents the inferred fields and tags present in the logs.

About Imandra Inc.

Imandra is the world leader in cloud-native automated reasoning technology.

For further information, see https://www.imandra.ai.