Imandra Protocol Language®

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

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.

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.

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 of the applications.

Successful Integration

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

Successful Integration

Features

Encoding your system interface in IPL paves the 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 the validity of the models.

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 directly built into the VS Code plugin.

Other services which require translation of IPL into Imandra:

As the famous quip goes, testing can reveal the presence of bugs but not their absence. This is why our clients formally verify their design to cover infinitely many possible inputs and scenarios to ensure the design meets everyone's expectations - business users, compliance, sales, and regulators. Historically, formal verification was reserved for highly specialized teams of PhDs at places like NASA. Imandra brings Formal Verification to mass software development.

Simulation - IPL model represents infinitely many possible behaviors. 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 the deep safety and reachability properties of the model.

How it works

Modeling system interfaces

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 - a 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 are internal system events that 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 respond 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 features 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.

Automated test case generation

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 Simulators

User Interfaces

VS Code

The VSCode interface for IPL provides a sophisticated IDE environment to develop precise specifications that generally correspond 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
VS Code

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.

VS Code

Decomposition Task manager

IPL specs are submitted to our cloud for in-depth 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.

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 your suite's coverage as a subset of the whole state-space at a glance.

State map (graph view)

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.

Simulators

Other language features

Custom library development

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

Intelligent code autocompletion

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

Context-aware help

The language will highlight any missing required fields that your model must support:

Local records

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

Float type precisions

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

Library Documentation

Access documentation with a mouse-over:

Type checking

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

Validation on duplicate titles

User cannot introduce two fields with the same title - an error will be thrown by the editor:

Custom fields and enums

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

Check out our Imandra Connectivity® page

Let's talkTalk
to an Expert

Schedule
a contact

Not sure
if we can help?

We'd be happy to discuss your project to suggest the best solution.

Schedule
a case analysis