Imandra Protocol Language®

Language and AI-powered tools for complex system interface modeling, simulation, testing and audit.

New!
Check out our new 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 (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. 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.

IPL Systems Integration Diagram
Icon-Speed

Speed

IPL is a domain-specific language for system interfaces. With its features and tools, you can model even the most complex systems in no time.

Icon-Precision

Precision

Safety-critical industries depend on precision - with IPL's approach for modeling infinite state machines, you create faithful and mathematically precise models of your system.

Icon-Rigor

Rigor

By construction, IPL models are susceptible to automated reasoning by Imandra. Algorithm state-space decomposition, model checking, test case generation and simulation are just some of many applications.

Features

Encoding your system interface in IPL paves way for many powerful features that historically were impossible. An IPL model may be converted into a simulator, used to visually state-space of the model, generate test cases and documentation, and much more. We also have tools for checking validity of the models.

IPL Features

How it works

IPL can be thought of as a domain-specific interface language to Imandra. For example, a model of 300 lines of IPL code will be translated to roughly 3,500 lines of Imandra code. Because of the precision of IPL, namely its strong type system and various model checking tools, it may be automatically translated into Imandra.

Some services like type checking and documentation generation (and other model analysis tools like reference counting) are built into the VS Code plugin directly.

Other services which require translation of IPL into Imandra:

Simulation - IPL model represents infinitely many possibilities. When on-demand simulators are created, Imandra treats the model as a complex set of constraints to faithfully simulate the actual system.

Test generation - automated state-space exploration and test case generation using Imandra's Region Decomposition.

Model checking - Imandra can answer deep safety and reachability properties of the model.

IPL - how does it work

Modeling system interfaces

IPL models system interfaces as infinite state machines - these are powerful analogs to Finite State Machines (FSM) which 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.

Modeling system interfaces

Automated test case generation

Automated test case generation is one of the most sought after feature of IPL. 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

On-demand Simulators

When an IPL model is translated into Imandra, one of its use cases is that it presents a powerful system of constraints which Imandra utilizes to create on-demand simulators. One of Imandra’s features is a powerful constraint-solving which is used by the simulators to faithfully replicate the entire systems as described by the IPL model. Such simulators may be created on-demand and run in the cloud during a DevOps process.

On demand simulator

User Interfaces

VS Code

The VSCode interface for IPL provides a sophisticated IDE environment in which to develop precise specifications which correspond generally to state transition systems, such as those described by Rules of Engagement (ROE) documents. Within the IDE it is possible to see domain specific hints on hover, exploit context-aware auto-completion and see detailed validation error and warning messages. Once an IPL document is free of validation errors in the IDE it is then possible to perform analysis by Imandra.

Download VS Code plugin
IPL VS code example
IPL terminal code example

Terminal

We also provide a command-line interface for submitting and managing IPL analysis jobs and simulator instances. This is a useful tool for integrating IPL into large organizations where your users use IPL across many different instances.

IPL terminal code example

Decomposition Task manager

IPL specs are submitted to our cloud for deep analysis by Imandra so our scalable infrastructure can do the heavy lifting. Use our web interface to get feedback on spec validation, guide automatic test case generation, and share the results of completed submissions with other members of your team.

IPL Decomposition Task Manager
IPL Decomposition Task Manager

State map (graph view)

Explore the logical state space of your IPL spec using Imandra's interactive state map. View constraints and state properties, and run queries against the state space to understand and identify particular states of interest. Select a set of states to make up your test suite, and see the coverage of your suite as a subset of the whole state space at a glance.

IPL Decomposition Task Manager

Simulators

IPL-generated simulators have web-based interfaces so you can connect to each instance and view the current session state and parameters. There are also numerous ways you can manage the parameters of the simulation.

IPL Simulators example

Other language features

Custom library development
IPL allows you to create your own libraries for specific domains and access them with a library command:

Custom library development

Intelligent code autocompletion
Look up available fields and values with built-in editor autocompletion:

Intelligent code autocompletion

Context-aware help
The language will highlight any missing required fields that your model must support:

Context-aware help

Local records
Locally declared records with linkable fields to messages and record types from FIX data dictionary:

Local records

Float type precisions
Explicitly set Float types (Qty, Price etc.) precision for your model:

Float type precisions

Library Documentation
Access documentation with a mouse-over:

FIX Documentation

Type checking
IPL is a strongly typed language, making it harder for you to introduce errors:

Type checking

Validation on duplicate names
User cannot introduce two fields with the same name - an error will be thrown by the editor:

Validation on duplicate names

Custom fields and enums
Extend the standard FIX enums, records and messages with custom entries:

Custom fields and enums
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