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 is a domain-specific language for system interfaces. With its features and tools, you can model even the most complex systems in no time.
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.
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.
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.
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 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 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 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.
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.
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.
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.
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 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.
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-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 names User cannot introduce two fields with the same name - an error will be thrown by the editor:
Custom fields and enums Extend the standard FIX enums, records and messages with custom entries: