Model Verification

In this section we give examples of verification that have been carried out on the implementation. Please use the menu on the right to view the relevant sections.

Overview and Status

In addition to the model source code, you will find a collection of Verification Goals (VGs). VGs are statements in IML expressing properties of the FIX engine model that we wish to verify. It’s important to note that IML is used for both building the model and describing the properties we wish to verify about it.

Consider the following quote from Volume 2 of the FIX 4.4 specification:

When either end of a FIX connection has not sent any data for [HeartBtInt] seconds, it will transmit a Heartbeat message.

One way to formalise that statement is to create two VGs:

VG.1.1 - any outbound message will result in an updated fe_last_time_data_sent field
VG.1.2 - any time update will result in check whether Heartbeat should be sent out

(* VG.1.1 *)
verify last_time_data_sent_gets_updated ( engine : fix_engine_state ) =
  let engine' = one_step ( engine ) in
  engine.outgoing_fix_msg = None && engine'.outgoing_fix_msg <> None
   ==>
  engine'.fe_last_time_data_sent = engine'.fe_curr_time
;;

(** VG.1.2 *)
let outbound_msg_heartbeat ( m : full_top_level_msg option ) =
  match m with
  | None      -> false
  | Some msg  ->
    match msg with
    | ValidMsg vmsg -> (
      match vmsg.full_msg_data with
      | Full_FIX_Admin_Msg admin_msg -> (
        match admin_msg with
        | Full_Msg_Hearbeat _        -> true
        | Full_Msg_Test_Request _    -> true
        | _                          -> false
      )
      | _ -> false
    )
    | _ -> false
;;

let time_update_received ( m, last_time_data_sent, hbeat_interval : fix_engine_int_msg option * fix_utctimestamp * fix_duration ) =
  match m with
  | None -> false
  | Some mint ->
    match mint with
    | TimeChange tc_data ->
       let valid_time = utctimestamp_add ( last_time_data_sent, hbeat_interval ) in
       utctimestamp_greaterThan ( tc_data, valid_time )
    | _ -> false
;;

verify hbeat_sent_if_no_data_received ( engine : fix_engine_state ) =
  let engine' = one_step ( engine ) in (
    engine.fe_curr_mode = ActiveSession
    && is_int_message_valid ( engine )
    && is_state_valid ( engine )
    && time_update_received ( engine.incoming_int_msg, engine.fe_last_time_data_sent, engine.fe_heartbeat_interval ) )
     ==>
    outbound_msg_heartbeat ( engine'.outgoing_fix_msg )
;;

It’s important to note that the ‘translation’ of the English-prose statements into IML (or other mathematically precise formal languages) may not be unique. The inherent ambiguity of natural languages is a major reason why the efforts of formalising protocol specifications must be collaborative and industry-wide.

Notice how this approach differs from traditional ‘testing’. In the statement above, we’re making a high-level claim about the model behaviour, and we can subject this claim to analysis over the entire system state-space. When Imandra analyses the model with respect to such a statement, it works to symbolically verify that the claim holds in all possible scenarios. When such a claim does not hold, Imandra works to construct a precise sequence of events (a “counterexample”) which exhibits a violation of the property.

VG Status

For updates, see the Announcements page.

Status as of May 21st, 2017:

Base

[x] VG.1 :: When in ActiveSession (normal mode) and receiving a non garbled and non session-level rejected message and the application is down. Such message would be sent back with a Business Reject.
[x] VG.2 :: FIX session should be terminated if the incoming sequence number is less than expected and the PossDupFlag is not set.
[x] VG.3 :: Messages that are garbled will be ignored (sequence counter will not be incremented).
[x] VG.4 :: Session rejected messages are rejected with the right reason and counter is incremented

Heartbeat Messages

[x] VG.1 :: “When either end of a FIX connection has not sent any data for [HeartBtInt] seconds, it will transmit a Heartbeat message.”
[x] VG.2 :: Non-garbled message updates the clock.
[x] VG.3 :: “When either end of the connection has not received any data for (HeartBtInt + “some reasonable transmission time”) seconds, it will transmit a Test Request message.”
[x] VG.4 :: “If there is still no Heartbeat message received after (HeartBtInt + ‘some reasonable transmission time’) seconds then the connection should be considered lost and corrective action be initiated.”

Logon Messages

[x] VG.1 :: “The logon message must be the first message sent by the application requesting to initiate a FIX session.”
[x] VG.2 :: *“The session acceptor must be prepared to immediately begin processing messages after receipt of the Logon.”
[x] VG.3 :: “After authentication, the initiator and acceptor must synchronize their messages through interrogation of the MsgSeqNum field before sending any queued or new messages.”
[x] VG.4 :: “If the session acceptor has chosen to change the session encryption key, the session initiator must send a third Logon back to the other side in order to acknowledge the key change request.”
[x] VG.5 :: NextExpectedMsgSeqNum is used correctly.

Logoff Messages

[ ] VG.1 :: * “Disconnection without the exchange of logout messages should be interpreted as an abnormal condition.”*
[ ] VG.2 :: “Before actually closing the session, the logout initiator should wait for the opposite side to respond with a confirming logout message.”
[ ] VG.3 :: “After sending the Logout message, the logout initiator should not send any messages unless requested to do so by the logout acceptor via a ResendRequest.”

Sequence Reset Messages

[x] VG.1 :: “When the incoming sequence number does not match the expected corrective processing is required. Note that the SeqReset-Reset message (used only to recover from a disaster vs. normal resend request processing) is an exception to this rule as it should be processed without regards to its MsgSeqNum.”
[ ] VG.2 :: “The Sequence Reset can only increase the sequence number. If a sequence reset is received attempting to decrease the next expected sequence number the message should be rejected and treated as a serious error.”

Sequence Number Logic

[x] VG.1 :: “Must always be the first message transmitted. Authenticate and accept the connection. After sending a Logon confirmation back, send a ResendRequest if a message gap was detected in the Logon sequence number.”
[x] VG.2 :: Out of sequence message would result in state transitioning into Recovery mode.
[ ] VG.3 :: “Ignore the incoming sequence number. The NewSeqNo field of the SeqReset message will contain the sequence number of the next message to be transmitted.”
[ ] VG.4 :: Application messages that result in a gap, we’ll transition into gap fill state.

Rejection Logic

[x] VG.1 :: * “During the gap fill process, certain administrative messages should not be retransmitted. Instead, a special SeqReset-GapFill message is generated.”*

Heartbeat Messages

This section contains verification goals for Hearbeat messages.

Heartbeat VG.1

“When either end of a FIX connection has not sent any data for [HeartBtInt] seconds, it will transmit a Heartbeat message.”

Notes: we transform this statement into 2 VGs:

VG.1.1 - any outbound message will result in an updated fe_last_time_data_sent field
VG.1.2 - any time update will result in check whether Heartbeat should be sent out

verify last_time_data_sent_gets_updated ( engine : fix_engine_state ) =
 let engine' = one_step ( engine ) in
 ( engine.outgoing_fix_msg = None && engine'.outgoing_fix_msg <> None )
  ==> (engine'.fe_last_time_data_sent = engine'.fe_curr_time )
;;

let outbound_msg_heartbeat ( m : full_top_level_msg option )=
 match m with 
 | None  -> false
 | Some msg  ->
 match msg with
 | ValidMsg vmsg -> (
  match vmsg.full_msg_data with 
  | Full_FIX_Admin_Msg admin_msg  -> (
   match admin_msg with 
   | Full_Msg_Hearbeat _       -> true
   | Full_Msg_Test_Request _   -> true
   | _                         -> false
   )
  | _ -> false
  )
 | _ -> false
;;

let time_update_received ( m, last_time_data_sent, hbeat_interval : fix_engine_int_msg option * fix_utctimestamp * fix_duration ) =
 match m with
 | None -> false
 | Some mint -> 
 match mint with 
 | TimeChange tc_data -> 
  let valid_time = utctimestamp_add ( last_time_data_sent, hbeat_interval ) in
  utctimestamp_greaterThan ( tc_data, valid_time )
 | _ -> false
;;

verify hbeat_sent_if_no_data_received ( engine : fix_engine_state ) =
 let engine' = one_step ( engine ) in ( 
 engine.fe_curr_mode = ActiveSession && 
 is_int_message_valid ( engine) && 
 is_state_valid ( engine ) && 
 time_update_received ( engine.incoming_int_msg, engine.fe_last_time_data_sent, engine.fe_heartbeat_interval ) )
 ==> outbound_msg_heartbeat ( engine'.outgoing_fix_msg )
;;

Heartbeat VG.2

Notes: there’s no mention of what constitutes a successful data - i.e. is it a non-garbled (but still rejected message)? We interpret this here as that a Non-garbled message results in update of data received.

Also, it’s important to note that we would not process an incoming message if the engine is in a Retransmit or CacheReplay mode, hence we use let incoming_processed = engine.incoming_fix_msg <> engine'.incoming_fix_msg

let incoming_is_not_garbled ( m : full_top_level_msg option ) = 
 match m with 
 | None -> false
 | Some msg ->
 match msg with
 | Garbled -> false
 | _ -> true
;;

verify non_garbled_updates_clock ( engine : fix_engine_state ) =
 let engine' = one_step (engine) in 
 let received_ts_correct =  ( engine.fe_curr_time = engine'.fe_last_data_received ) in 
 let incoming_processed = engine.incoming_fix_msg <> engine'.incoming_fix_msg in 
 ( incoming_is_not_garbled ( engine.incoming_fix_msg ) && incoming_processed) ==> received_ts_correct
;;

Heartbeat VG.3

‘When either end of the connection has not received any data for (HeartBtInt + “some reasonable transmission time”) seconds, it will transmit a Test Request message.’

Notes: ‘reasonable time’ is represented by a ‘duration’ type field fe_testreq_interval.

let no_heartbeats_received ( m, data_received, hbeat_interval, pad_interval : fix_engine_int_msg option * fix_utctimestamp * fix_duration * fix_duration ) =
 match m with
 | None -> false
 | Some mint -> 
 match mint with 
 | TimeChange tc_data -> 
  let valid_time = utctimestamp_add ( data_received, hbeat_interval ) in
  let valid_time_padded = utctimestamp_add ( valid_time, pad_interval ) in
  utctimestamp_greaterThan ( tc_data, valid_time_padded )
 | _ -> false
;;

let msg_is_test_request ( m : full_top_level_msg option ) =
 match m with 
 | None  -> false
 | Some msg ->
 match msg with
 | ValidMsg vmsg -> (
  match vmsg.full_msg_data with 
  | Full_FIX_Admin_Msg admin_msg  -> (
   match admin_msg with 
   | Full_Msg_Test_Request _  -> true
   | _ -> false
  )
  | _ -> false
 )
 | _ -> false
;;

verify test_request_sent_out ( engine : fix_engine_state ) =
 let engine' = one_step ( engine ) in
  ( is_int_message_valid ( engine ) &&
  is_state_valid ( engine ) &&
  engine.fe_curr_status = Normal && 
  engine.fe_curr_mode = ActiveSession && 
  no_heartbeats_received ( engine.incoming_int_msg,
                            engine.fe_last_data_received,
                            engine.fe_heartbeat_interval,
                            engine.fe_testreq_interval ) )
  ==>
  msg_is_test_request ( engine'.outgoing_fix_msg )
;;

Heartbeat VG.4

“If there is still no Heartbeat message received after (HeartBtInt + “some reasonable transmission time”) seconds then the connection should be considered lost and corrective action be initiated.”

Notes: note sure what ‘corrective action be initiated’ means, here we interpret it as meaning that a logoff message to be sent out, session closed and ‘status’ of the engine state set to ConnTerminatedWithoutLogoff.

let no_heartbeats_received_logoff ( m, data_sent_out, hbeat_interval, pad_interval : fix_engine_int_msg option * fix_utctimestamp * fix_duration * fix_duration ) =
 match m with
 | None -> false
 | Some mint -> 
 match mint with 
 | TimeChange tc_data -> 
  let valid_time = utctimestamp_add ( data_sent_out, hbeat_interval ) in
  let valid_time_padded = utctimestamp_add ( valid_time, pad_interval ) in
  utctimestamp_greaterThan ( tc_data, valid_time_padded )
 | _ -> false
;;

verify no_response_logoff ( engine : fix_engine_state ) =
 let engine' = one_step ( engine ) in
 (is_int_message_valid ( engine ) &&
  is_state_valid ( engine ) &&
  engine.fe_curr_mode = WaitingForHeartbeat && 
  no_heartbeats_received ( engine.incoming_int_msg, 
                            engine.fe_last_time_data_sent,
                            engine.fe_heartbeat_interval,
                            engine.fe_testreq_interval ) )
  ==>
  ( engine'.fe_curr_mode = NoActiveSession && 
   engine'.fe_curr_status = ConnTerminatedWithoutLogoff )
;;

Heartbeat VG.5

“If HeartBtInt is set to zero then no regular heartbeat messages will be generated. Note that a test request message can still be sent independent of the value of the HeartBtInt, which will force a Heartbeat message.”

Notes: We implement ‘test request message can still be sent independent of the value of the HeartBtInt’ as internal message.

let field_null ( f : int option ) =
 match f with 
 | None -> true
 | Some x -> x = 0
;;

let hbeat_interval_null ( interval : fix_duration ) =
 field_null ( interval.dur_years )   &&
 field_null ( interval.dur_months )  && 
 field_null ( interval.dur_days )    && 
 field_null ( interval.dur_hours )   &&
 field_null ( interval.dur_minutes ) &&
 field_null ( interval.dur_seconds )
;;

let hbeat_sent_if_no_data_received_new ( engine : fix_engine_state ) =
 let engine' = one_step ( engine ) in 
 ( engine.fe_curr_mode = ActiveSession && 
  is_valid_utctimestamp ( engine.fe_last_data_received ) && 
  is_int_message_valid ( engine) && is_state_valid ( engine ) && 
  time_update_received ( engine.incoming_int_msg, engine.fe_last_data_received, engine.fe_heartbeat_interval ) )
 ==> outbound_msg_heartbeat ( engine'.outgoing_fix_msg )
;;

Heartbeat VG.6

“Heartbeats issued as the result of Test Request must contain the TestReqID transmitted in the Test Request message. This is useful to verify that the Heartbeat is the result of the Test Request and not as the result of a regular timeout.”

Note: that the sequence number of the TestRequest message must be correct so that the state does not transition into Recovery.

let msg_is_test_request_id ( m, tr_id, seq_num : full_top_level_msg option * int * int ) =
 match m with 
 | None  -> false
 | Some msg ->
 match msg with
 | ValidMsg vmsg -> seq_num = vmsg.full_msg_header.h_msg_seq_num && (
  match vmsg.full_msg_data with 
  | Full_FIX_Admin_Msg admin_msg  -> (
   match admin_msg with 
   | Full_Msg_Test_Request data -> data.test_req_id = tr_id
   | _ -> false
  )
  | _ -> false
 )
 | _ -> false
;;

let correct_hbeat_sent ( m, tr_id : full_top_level_msg option * int ) =
 match m with
 | None -> false
 | Some msg ->
   match msg with 
   | ValidMsg vmsg -> (
    match vmsg.full_msg_data with 
    | Full_FIX_Admin_Msg admin_msg  -> (
     match admin_msg with 
     | Full_Msg_Hearbeat data ->  (
      match data.hb_test_req_id with 
      | None -> false
      | Some x -> x = tr_id
     )
    | _ -> false
   )
  | _ -> false
 )
 | _ -> false
;;

verify heartbeat_has_correct_id ( test_req_id, engine : int * fix_engine_state ) =
 let engine' = one_step ( engine ) in 
 ( test_req_id > 0 && 
   engine.incoming_int_msg = None && 
   engine.fe_curr_mode = ActiveSession && 
   engine.fe_application_up && 
   msg_is_test_request_id ( engine.incoming_fix_msg, test_req_id, engine.incoming_seq_num + 1) )
    ==> correct_hbeat_sent ( engine'.outgoing_fix_msg, test_req_id )
;;

Logon Messages

This section describes verification goals for Logon messages.

Logon VG.1

“The logon message must be the first message sent by the application requesting to initiate a FIX session.”

Note: we augment this with requirement that the engine correctly sets the acceptor/initiator flag.

let incoming_int_create_session ( m, targetID : fix_engine_int_msg option * int ) =
    match m with
    | None      -> false
    | Some msg  ->
    match msg with
    | CreateSession data    -> data.dest_comp_id = targetID
    | _                     -> false
;;

let state_is_init ( engine : fix_engine_state ) =
    engine.incoming_seq_num = 1 &&
    engine.outgoing_seq_num = 1 &&
    engine.fe_initiator = None &&
    engine.fe_curr_mode = NoActiveSession &&
    engine.fe_curr_status = Normal &&
    engine.fe_history = [] &&
    engine.fe_cache = []
;;

let outbound_msg_logon ( m, targetID : full_top_level_msg option * int ) =
    match m with
    | None      -> false
    | Some msg  ->
    match msg with
    | ValidMsg vmsg -> (
    let correct_target_id = vmsg.full_msg_header.h_target_comp_id = targetID in
    match vmsg.full_msg_data with
    | Full_FIX_App_Msg _        -> false
    | Full_FIX_Admin_Msg amsg   ->
    match amsg with
    | Full_Msg_Logon _          -> correct_target_id
    | _                         -> false
    )
    | _             -> false
;;

verify logon_msg_is_first ( engine, targetID : fix_engine_state * int ) =
    let engine' = one_step ( engine ) in
    ( state_is_init ( engine ) &&
    incoming_int_create_session ( engine.incoming_int_msg, targetID ) ) ==>
     ( outbound_msg_logon ( engine'.outgoing_fix_msg, targetID ) &&
     engine'.fe_curr_mode = LogonInitiated &&
     engine'.fe_initiator = Some true)
;;

Logon VG.2

“The session acceptor must be prepared to immediately begin processing messages after receipt of the Logon. The session initiator can choose to begin transmission of FIX messages before receipt of the confirmation Logon, however it is recommended that normal message delivery wait until after the return Logon is received to accommodate encryption key negotiation.”

(* Logon VG2.1 *)
let waiting_for_logon_ack ( engine : fix_engine_state ) =
    engine.fe_curr_mode = LogonInitiated
;;

let int_app_msg_exists ( m : fix_engine_int_msg option ) =
    match m with
    | None      -> false
    | Some _    -> true
;;

let no_msg_sent_until_logon_acked ( engine : fix_engine_state ) =
    let engine' = one_step ( engine ) in
    ( engine.fe_curr_mode = LogonInitiated && int_app_msg_exists ( engine' ))
    ==>
    ( engine'.outgoing_fix_msg = None )
;;

(* Logon VG2.2 *)
let incoming_logon_ack ( m, self_comp_id : full_top_level_msg option * int ) =
    match m with
    | None -> false
    | Some msg ->
    match msg with
    | ValidMsg vmsg -> (
        let valid_header = vmsg.full_msg_header.h_target_comp_id = self_comp_id in
        match vmsg.full_msg_data with
        | Full_FIX_App_Msg _ -> false
        | Full_FIX_Admin_Msg amsg -> (
            match amsg with
            | Full_Msg_Logon data -> valid_header
            | _ -> false
         )
     )
    | _ -> false
;;

verify receive_logon_ack ( engine : fix_engine_state ) =
    let engine' = one_step ( engine ) in
    ( incoming_logon_ack ( engine.incoming_fix_msg, engine.fe_comp_id ) &&
        engine.fe_curr_mode = LogonInitiated &&
        engine.fe_cache = [] &&
        is_state_valid ( engine ) )
    ==>
    ( engine'.fe_curr_mode = ActiveSession )
;;

Logon VG.3

“After authentication, the initiator and acceptor must synchronize their messages through interrogation of the MsgSeqNum field before sending any queued or new messages. A comparison of the MsgSeqNum in the Logon message to the internally monitored next expected sequence number will indicate any message gaps. Likewise, the initiator can detect gaps by comparing the acknowledgment Logon message’s MsgSeqNum to the next expected value. The section on message recovery later in this document deals with message gap handling.”

let logon_msg_out_of_sequence ( m : full_top_level_msg option ) =
    true
;;

verify when_gap_detected_request_is_sent ( engine : fix_engine_state ) =

    let engine' = one_step ( engine ) in

    logon_msg_out_of_sequence ( engine )
        ==>
    ( test_request_sent ( engine' ) && engine'.fe_curr_mode = Recovery )
;;

Logon VG.4

“If the session acceptor has chosen to change the session encryption key, the session initiator must send a third Logon back to the other side in order to acknowledge the key change request. This also allows the session acceptor to know when the session initiator has started to encrypt using the new session key. Both parties are responsible for infinite loop detection and prevention during this phase of the session.”

Notes: we break up the statement into the following VGs:

4.1 - If a confirmation Logon is received with a different encryption key, then another Logon is sent back with the same key. Also, we increment the ‘fe_num_logons_sent’ counter.
4.2 - When the engine attempts to send out a Logon message when the count is violated, it would transition into error mode with status change.

let received_logon_diff_key ( m, self_comp_id, encrypt_method : full_top_level_msg option * int * fix_encryption_method ) =
    match m with
    | None -> true
    | Some msg ->
    match msg with
    | ValidMsg vmsg -> (
        let valid_header = vmsg.full_msg_header.h_target_comp_id = self_comp_id in
        match vmsg.full_msg_data with
        | Full_FIX_App_Msg _ -> false
        | Full_FIX_Admin_Msg amsg -> (
            match amsg with
            | Full_Msg_Logon data -> valid_header && ( data.ln_encrypt_method = encrypt_method )
            | _ -> false
         )
    )
    | _ -> false
;;

let logon_sent_out ( m, encrypt_method : full_top_level_msg option * fix_encryption_method ) =
    match m with
    | None -> true
    | Some msg ->
    match msg with
    | ValidMsg vmsg -> (
        match vmsg.full_msg_data with
        | Full_FIX_App_Msg _ -> false
        | Full_FIX_Admin_Msg amsg -> (
            match amsg with
            | Full_Msg_Logon data -> data.ln_encrypt_method = encrypt_method
            | _ -> false
         )
    )
    | _ -> false
;;

(** Logon VG.4.1 *)
verify encrypt_key_different_logon_sent ( engine, new_encrypt_method : fix_engine_state * fix_encryption_method ) =
    let engine' = one_step ( engine ) in
    (   engine.fe_cache = [] &&
        engine.fe_curr_mode = LogonInitiated &&
        engine.fe_encrypt_method <> new_encrypt_method &&
        received_logon_diff_key ( engine.incoming_fix_msg, engine.fe_comp_id, new_encrypt_method ) &&
        engine.fe_num_logons_sent < engine.fe_max_num_logons_sent
    ) ==> (
        logon_sent_out ( engine'.outgoing_fix_msg, new_encrypt_method ) &&
        engine'.fe_encrypt_method = new_encrypt_method &&
        engine'.fe_num_logons_sent = (1 + engine.fe_num_logons_sent)
    )
;;

(** Logon VG.4.2 *)
verify max_num_logons_breached_error ( engine : fix_engine_state ) =
    let engine' = one_step ( engine ) in
    ( received_logon_diff_key ( engine ) &&
        ( engine.fe_num_logons_sent = engine.fe_max_num_logons_sent ) )
    ==>
    ( engine'.fe_curr_mode = Error &&
        engine'.fe_curr_status = MaxNumLogonMsgsViolated )
;;

Logon VG.5

“NextExpectedMsgSeqNum (789) is used as follows: In its Logon request the session initiator supplies in NextExpectedMsgSeqNum (789) the value next expected from the session acceptor in MsgSeqNum (34). The outgoing header MsgSeqNum (34) of the Logon request is assigned the next-to-be-assigned sequence number as usual.

The session acceptor validates the Logon request including that NextExpectedMsgSeqNum (789) does not represent a gap. It then constructs its Logon response with NextExpectedMsgSeqNum (789) containing the value next expected from the session initiator in MsgSeqNum (34) having incremented the number above the Logon request if that was the sequence expected. The outgoing header MsgSeqNum (34) is constructed as usual. The session initiator waits to begin sending application messages until it receives the Logon response. When it is received the initiator validates the response including that NextExpectedMsgSeqNum (789) does not represent a gap.

Both sides react to NextExpectedMsgSeqNum (789) from its counterparty thus:

If equal to the next-to-be-assigned sequence, proceed sending new messages beginning with that number.
If lower than the next-to-be-assigned sequence, ‘recover’ (see ‘Message Recovery’) all messages from the the last message delivered prior to this Logon through the specified NextExpectedMsgSeqNum (789) sending them in order; then Gap Fill over the sequence number used in Logon and proceed sending newly queued messages with a sequence number one higher than the original Logon.
If higher than the next-to-be-assigned sequence, send Logout to abort the session.

Neither side should generate a ResendRequest based on MsgSeqNum (34) of the incoming Logon message but should expect any gaps to be filled automatically. If a gap is produced by the Logon message MsgSeqNum (34), the receive logic should expect the gap to be filled automatically prior to receiving any messages with sequences above the gap.”

let is_next_expected_msg_seq_num_present ( m, next_seq_num : full_top_level_msg option * int ) =
    match m with
    | None -> true
    | Some msg ->
    match msg with
    | ValidMsg vmsg -> (
        match vmsg.full_msg_data with
        | Full_FIX_App_Msg _ -> false
        | Full_FIX_Admin_Msg amsg -> (
            match amsg with
            | Full_Msg_Logon data ->  (
                match data.ln_next_expected_msg_seq_num with
                | None -> false
                | Some seq_num -> seq_num = next_seq_num
            )
            | _ -> false
         )
    )
    | _ -> false
;;

Base

Base VG.1

When in ActiveSession (normal mode) and receiving a non grabled and non session-level rejected message and the application is down. Such message would be sent back with a Business Reject.

let msg_is_biz_reject = function  | Some (ValidMsg msg_data) ->
    begin match msg_data.full_msg_data with
      | Full_FIX_Admin_Msg (Full_Msg_Business_Reject _) -> true
      | _ -> false
    end
  | _ -> false
;;

let msg_is_valid = function
  | Some (ValidMsg _) -> true
  | _ -> false
;;

verify app_down_get_biz_reject ( state : fix_engine_state ) =
  let incoming_biz_rejected = msg_is_valid ( state.incoming_fix_msg ) in
  let no_incoming_msgs = state.incoming_int_msg = None in
  let state' = one_step (state) in
  let result_biz_reject = msg_is_biz_reject ( state'.outgoing_fix_msg ) in
  ( state.fe_cache = []
    && incoming_biz_rejected && not (state.fe_application_up)
    && state.fe_curr_mode = ActiveSession && no_incoming_msgs )
  ==>
  result_biz_reject
;;

Base VG.2

From Vol 2. Page 9:

In *ALL cases except the Sequence Reset - message, the FIX session* should be terminated if the incoming sequence number is less than expected and the PossDupFlag is not set. A Logout message with some descriptive text should be sent to the other side before closing the session.

let poss_dup_flag_not_set ( flag : bool option ) =
  flag = None
;;

let incoming_msg_not_valid ( msg, state_inc_seq_num : full_top_level_msg option * int ) =
  match msg with
  | Some (ValidMsg vmsg) ->
    let seq_num_incorrect = vmsg.full_msg_header.h_msg_seq_num < state_inc_seq_num in
    let msg_is_seq_reset =
      begin match vmsg.full_msg_data with
        | Full_FIX_Admin_Msg (Full_Msg_Sequence_Reset _) -> true
        | _ -> false
      end
    in
    (seq_num_incorrect && msg_is_seq_reset
     && poss_dup_flag_not_set ( vmsg.full_msg_header.h_poss_dup_flag ))
  | _   -> false
;;

let msg_is_logout = function
  | Some (ValidMsg vmsg) ->
    begin match vmsg.full_msg_data with
      | Full_FIX_Admin_Msg (Full_Msg_Logoff _) -> true
      | _ -> false
    end
  | _ -> false
;;

verify less_seq_num_logout ( state : fix_engine_state ) =
  let no_incoming_int_msgs = state.incoming_int_msg = None in
  let state_good = not ( state.fe_application_up ) && ( state.fe_curr_mode = ActiveSession ) in
  let state' = one_step (state) in
  ( state.fe_application_up && no_incoming_int_msgs && state_good && state.fe_cache = [] &&
    incoming_msg_not_valid ( state.incoming_fix_msg, 1 ) )
  ==> msg_is_logout ( state'.outgoing_fix_msg )
;;

Base VG.3

Messages that are garbled will be ignored (sequence counter will not be incremented).

let incoming_msg_garbled = function
  | Some (Garbled) -> true
  | _ -> false
;;

verify garbled_are_ignored ( state : fix_engine_state ) =
  let state' = one_step (state) in
  let msg_ignored = ( state' =  { state with incoming_fix_msg = None } ) in
  let no_internal_msgs = state.incoming_int_msg = None in
  let no_cache_replay_or_retransmit = not ( state.fe_curr_mode = CacheReplay || state.fe_curr_mode = Retransmit ) in
  ( incoming_msg_garbled (state.incoming_fix_msg)
    && no_cache_replay_or_retransmit
    && no_internal_msgs )
  ==> msg_ignored
;;

Base VG.4

Session rejected messages are rejected with the right reason and counter is incremented.

let incoming_msg_session_reject = function
  | Some (SessionRejectedMsg _) -> true
  | _ -> false
;;

let msg_is_reject = function
  | Some (ValidMsg vmsg) ->
    begin match vmsg.full_msg_data with
      | Full_FIX_Admin_Msg (Full_Msg_Reject _) -> true
      | _ -> false
    end
  | _ -> false
;;

(** Note that it's important to remember that a message may only be rejected if we're in ActiveSession state.
    It would be otherwise ignore (if in NoActiveSession state) or not processed if the engine is in CacheReplay or
    Retransmit modes. *)
verify session_rejects_are_rejected ( state : fix_engine_state ) =
  let no_incoming_int_msgs = state.incoming_int_msg = None in
  let incoming_rejected = incoming_msg_session_reject ( state.incoming_fix_msg ) in
  let state' = one_step (state) in
  let msg_rejected = msg_is_reject ( state'.outgoing_fix_msg ) in
  let seq_num_updated = ( ( state.outgoing_seq_num + 1 ) = state'.outgoing_seq_num ) in
  ( no_incoming_int_msgs && incoming_rejected && state.fe_curr_mode = ActiveSession)
  ==>
  ( msg_rejected && seq_num_updated )
;;

Rejection Logic

Sequence Number Logic

Sequence Reset Messages

Seq_Reset VG.1

“When the incoming sequence number does not match the expected corrective processing is required. Note that the SeqReset-Reset message (used only to recover from a disaster vs. normal resend request processing) is an exception to this rule as it should be processed without regards to its MsgSeqNum.”

let inc_msg_seqreset_reset ( m : full_top_level_msg option ) =
    match m with
    | None -> false
    | Some msg ->
    match msg with
    | ValidMsg vmsg -> (
        match vmsg.full_msg_data with
        | Full_FIX_App_Msg _ -> false
        | Full_FIX_Admin_Msg amsg -> (
            match amsg with
            | Full_Msg_Sequence_Reset data -> (
                (* A missing flag or flag = No tells us that message of the Reset mode. *)
                match data.seqr_gap_fill_flag with | None -> true | Some f -> f = FIX_No
             )
            | _ -> false
         )
    )
    | _ -> false
;;

let state_updated ( engine, new_seq_num : fix_engine_state * int ) =
    engine.incoming_seq_num = new_seq_num &&
    engine.fe_curr_mode = ActiveSession &&
    engine.fe_cache = []
;;

let out_of_seq_seqreset_processed ( engine, new_seq_num : fix_engine_state * int ) =
    let engine' = one_step ( engine ) in
    (   inc_msg_seqreset_reset ( engine.incoming_fix_msg ) &&
        engine.fe_curr_mode <> NoActiveSession &&
        engine.fe_cache = []
    ) ==> (
        state_updated ( engine', new_seq_num )
    )
;;