Tutorials

These tutorials will show incrementally how to create an ipl file, which represents the correct protocol for receving and sending FIX messages for a particular venue or trading system. We show how we model the ipl file as a state transition system which tracks the progress of a particular order. In the state of the system it is important to remember that all the information pertains to one order for the examples we show here. It is possible to model more complicated systems, but for the purposes of our exposition it is most useful to simply consider one order.

• Basic Model
• Introducing State
• Adding Actions
• Custom Message Fields and Cases
• Repeating Groups
• Advanced Features
• Multiple Imports

Declaring Message Flows

Imandra can automatically produce test cases and regions for analysis. Message Flows are a way of declaring a sequence of events which are of interest for analysis.

In each section of the tutorial we define a message flow, which allows us to link the model to a browser demonstrating graphically an analysis performed by Imandra.