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.
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.
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.
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.
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.
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.
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
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.
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.
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.
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.
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
We work with many of the world's largest and most trusted brands, universities and government agencies.
And we would be delighted to work with you.
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.
Schedulea case analysis