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:
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:
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:
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.
VS Code IPL Plugin in action
About Imandra Inc.
Imandra is the world leader in cloud-native automated reasoning technology.
For further information, see https://www.imandra.ai.