%
% Simplified model of the TTE clock synchronization algorithm.
%
% Author: Bruno Dutertre, SRI International. 2011
%
% References:
%
%  "Integrated Formal Analysis of Timed-Triggered Ethernet",
%   Bruno Dutertre, Natarajan Shankar, and Sam Owre, NASA Contractor Report
%   (to appear).
%
%  "Timed-Triggered Ethernet. SAE Aerospace Standard, AS 6802, v1.1.2, 2011"
%
%  "Automated Formal Verification of the TTEthernet Synchronization
%   Quality" by Wilfried Steiner and Bruno Dutertre, NFM 2011.
%
%
% Specific instance in this file:
% - five SMs
% - two CMs
% - one Byzantine faulty SM
% - the CM compression function uses the midpoint if 5 clock readings
%   are received
%

tte_synchro: CONTEXT =

BEGIN

  POSREAL: TYPE = { x:REAL | x > 0 };

  %
  % max_drift is a bound on the maximal drift 
  % experienced by a clock in one synchronization interval.
  % This drift is relative to real time.
  %
  max_drift: POSREAL;

  %
  % Clock value = any real
  %
  CLOCK: TYPE = REAL;

  %
  % N = number of Synchronization Masters (SMs)
  % M = number of Compression Masters (CMs)
  %
  N: NATURAL = 5;
  M: NATURAL = 2;

  SM_ID: TYPE = [1 .. N];
  CM_ID: TYPE = [1 .. M];

  %
  % Component status
  % - good: not faulty
  % - omissive: inconsistent omission
  % - byzantine: inconsistent value + omission
  %
  STATUS: TYPE = { good, omissive, byzantine };

  %
  % Status of each SM
  % - for this scenario, we assume SM[3] is byzantine
  % - the other SMs are good
  %
  sm_status(i: SM_ID): STATUS = IF i=3 THEN byzantine ELSE good ENDIF;


  %
  % Status of each CM (not used for now)
  %
  cm_status(i: CM_ID): STATUS = good;
  

  %-------------------------------------------------------------------
  % Sort predicate for the compression function:
  % - a CM receives at most N values c[1] to c[N]
  % - boolean array v indicates which values are present
  %   v[i] = false means that i is omissive (or byzantine) and the
  %   value from i was not received.
  %
  % The compression function is defined by the number of
  % valid values received and the order of the valid values.
  %
  % Predicate sort(c, v, n, p) holds if
  % 1) there are n valid values in c[1 ... N] (i.e.
  %    n of the booleans v[1] ... v[N] are true)
  % 2) p is a permutation of the SM indices
  % 3) p[1] ... p[n] enumerates the n valid values of 
  %    c[1 ... N] in increasing order
  %--------------------------------------------------------------------

  sort(c: ARRAY SM_ID OF CLOCK, v: ARRAY SM_ID OF BOOLEAN,
       n: [0 .. N], p: ARRAY SM_ID OF SM_ID): BOOLEAN =
        (FORALL (i: SM_ID): i<n => c[p[i]] <= c[p[i+1]])
    AND (FORALL (i: SM_ID): v[p[i]] <=> (i <= n))
    AND (FORALL (i, j: SM_ID): p[i] = p[j] => i = j);


  %---------------------------------------------------------
  % Synchronization master
  %
  % Three states: send, correct, drift.
  %
  % States send and correct model the resynchronization
  % protocol at the beginning of every interval:
  % 1) in state send: the SM sends its clock to the CMs
  % 2) in state correct: the SM applies a clock correction
  %    based on the compression values it gets from the CMs
  %
  % In state drift: the SM clock drifts from real-time (this
  % models the rest of the resynchronization interval).
  %---------------------------------------------------------

  SM_STATE: TYPE = { sm_send, sm_correct, sm_drift };

  SM: MODULE =
    BEGIN
      INPUT
        compression: ARRAY CM_ID OF CLOCK

      OUTPUT
        state: SM_STATE,
        clock: CLOCK

      INITIALIZATION
        state = sm_send;
        clock = 0;

      TRANSITION
        [ state = sm_send --> 
            state' = sm_correct;

       [] state = sm_correct -->
            state' = sm_drift;
            clock' = (compression[1] + compression[2])/2; % correction

       [] state = sm_drift -->
            clock' IN { x : CLOCK | clock - max_drift <= x AND x <= clock + max_drift };
            state' = sm_send;
       ]
     END;

  
 
   %------------------------------------------------------------------
   % Compression master
   %
   % Three states: receive, correct, drift
   %
   % States receive and correct model the resynchronization
   % protocol:
   % 1) in state receive, each CM gets clock readings from the CMs
   %    and computes a compression value
   % 2) in state correct, each CM corrects its clock to 
   %    the compression value
   %
   % In state drift: the clock drift by some amount bounded
   % by max_drift.
   %
   % To model possible missing input (from faulty SMs), we use 
   % a boolean array 'sm_valid': sm_valid[i] is true if the CM
   % receives a value from SM i (i.e., sm_reading[i] is taken
   % into account when computing the compression).
   %------------------------------------------------------------------
 
   CM_STATE: TYPE = { cm_receive, cm_correct, cm_drift };

   CM: MODULE =
     BEGIN
       INPUT
         sm_reading: ARRAY SM_ID OF CLOCK,
	 sm_valid: ARRAY SM_ID OF BOOLEAN

       LOCAL
	 perm: ARRAY SM_ID OF SM_ID

       OUTPUT
         state: CM_STATE,
         clock: CLOCK,
         compression: CLOCK

       INITIALIZATION
         state = cm_receive;
         compression = 0;
         clock = 0;

       DEFINITION
         perm IN { p: ARRAY SM_ID OF SM_ID | TRUE };

       TRANSITION
         [ state = cm_receive AND sort(sm_reading, sm_valid, 3, perm') -->
             %% received 3 clock readings (i.e., two faulty SMs)
             state' = cm_correct;
             compression' = sm_reading[perm'[2]];

        [] state = cm_receive AND sort(sm_reading, sm_valid, 4, perm')  -->
	     %% received 4 clock readings
             state' = cm_correct;
             compression' = (sm_reading[perm'[2]] + sm_reading[perm'[3]])/2;

        [] state = cm_receive AND sort(sm_reading, sm_valid, 5, perm') -->
             %% received 5 clock readings
             state' = cm_correct;
             compression' = sm_reading[perm'[3]];

        [] state = cm_correct -->
             clock' = compression;
             state' = cm_drift;
    
        [] state = cm_drift -->
             clock' IN { x : CLOCK | clock - max_drift <= x AND x <= clock + max_drift };
             state' = cm_receive;
        ]
     END;



  %--------------------------------------------------------------
  % Connection and fault model
  % - the input is a vector of N clock values (from the N SMs)
  % - the clock value received by CM j from SM i is 
  %   modeled by the pair (sm_reading[j][i], sm_valid[j][i])
  %   depending on i's status.
  %
  % If i is good then 
  %    sm_reading[j][i] = clock[i]
  %    sm_valid[j][i] is true
  %
  % If i is omissive then
  %    sm_reading[j][i] = clock[i]
  %    sm_valid[j][i] can be anything
  %
  % If is is Byzantine then
  %    sm_reading[j][i] can be anything
  %    sm_valid[j][i] can be anything
  %--------------------------------------------------------------

  Connection: MODULE =
    BEGIN
      INPUT
        sm_clock: ARRAY SM_ID OF CLOCK
      OUTPUT
        sm_reading: ARRAY CM_ID OF ARRAY SM_ID OF CLOCK,
        sm_valid: ARRAY CM_ID OF ARRAY SM_ID OF BOOLEAN
  
      DEFINITION
        %% sm_valid[j][i] is true if i is GOOD
        sm_valid IN { B: ARRAY CM_ID OF ARRAY SM_ID OF BOOLEAN |
                      FORALL (j: CM_ID, i: SM_ID): 
                        sm_status(i) = good => B[j][i] };

        %% sm_reading[j][i] is equal to sm_clock[i] unless i is Byzantine
        sm_reading IN { A: ARRAY CM_ID OF ARRAY SM_ID OF CLOCK |
                        FORALL (j: CM_ID, i: SM_ID): 
                           sm_status(i) /= byzantine => A[j][i] = sm_clock[i] };
    END;
 

  %--------------
  % Full system
  %--------------

  % All SMs
  SMs: MODULE = 
     WITH OUTPUT sm_clock: ARRAY SM_ID OF CLOCK,
                 sm_state: ARRAY SM_ID OF SM_STATE
      (|| (i: SM_ID):
            RENAME 
              clock TO sm_clock[i],
              state TO sm_state[i]
            IN SM);

  % All CMs
  CMs: MODULE = 
     WITH INPUT sm_reading: ARRAY CM_ID OF ARRAY SM_ID OF CLOCK,
                sm_valid: ARRAY CM_ID OF ARRAY SM_ID OF BOOLEAN;

          OUTPUT compression: ARRAY CM_ID OF CLOCK,
                 cm_state: ARRAY CM_ID OF CM_STATE,
                 cm_clock: ARRAY CM_ID OF CLOCK

       (|| (i: CM_ID):
             RENAME
               compression TO compression[i],
               state TO cm_state[i],
               clock TO cm_clock[i],
               sm_reading TO sm_reading[i],
               sm_valid TO sm_valid[i]
             IN CM);

  % Full system
  TTE: MODULE = SMs || CMs || Connection;



  %--------------
  %  Properties
  %--------------

  %
  % Auxiliary lemmas:  phase1 to phase3 can all be proved by induction at depth 2
  %
  phase1: LEMMA TTE |-
     G(FORALL (i: SM_ID, j: CM_ID): sm_state[i] = sm_send <=> cm_state[j] = cm_receive);

  phase2: LEMMA TTE |-
     G(FORALL (i: SM_ID, j: CM_ID): sm_state[i] = sm_correct <=> cm_state[j] = cm_correct);

  phase3: LEMMA TTE |-
     G(FORALL (i: SM_ID, j: CM_ID): sm_state[i] = sm_drift <=> cm_state[j] = cm_drift);


  %
  % The SMs are synchronized within 2 * max_drift (which is the best we can do).
  % This holds in this model because all SMs receive the same pair of compression 
  % values and apply the exact same correction.
  %
  % The lemma is provable by induction at depth 2 using phase1 as a lemma
  % (or using phase2 or phase3 as lemma)
  %
  sm_clock_distance: LEMMA
     TTE |- G(FORALL (i, j: SM_ID): sm_clock[i] - sm_clock[j] <= 2 * max_drift);

  % this one is obviously false (counterexamples at depth 3)
  sm_clock_distance_strict: LEMMA
     TTE |- G(FORALL (i, j: SM_ID): sm_clock[i] - sm_clock[j] < 2 * max_drift);



  %
  % The CMs are synchronized within 4 * max_drift
  %

  %
  % The next lemmas are not true: there are counterexamples at depth 6
  %
  cm_clock_distance1: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= 3 * max_drift);

  cm_clock_distance1a: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= (7/2) * max_drift);

  cm_clock_distance1b: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= (15/4) * max_drift);

  cm_clock_distance1c: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= (31/8) * max_drift);

  cm_clock_distance1d: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= (63/16) * max_drift);

  cm_clock_distance1e: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= (127/32) * max_drift);


  %
  % The next lemma is true: it's provable by induction at depth 3
  % using sm_clock_distance and phase1 as lemmas.
  %
  cm_clock_distance2: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] <= 4 * max_drift);

  %
  % The next lemmas is false: this shows that 4 * max_drift is the best we can do
  %
  cm_clock_distance2_strict: LEMMA
     TTE |- G(FORALL (i, j: CM_ID): cm_clock[i] - cm_clock[j] < 4 * max_drift);




  %
  % Synchronization between CMs and SMs: 3 * max_drift
  %
  sm_cm_clock_distance: LEMMA
     TTE |- G(FORALL (i: SM_ID, j: CM_ID):
                  sm_clock[i] - cm_clock[j] <= 3 * max_drift AND 
                  cm_clock[j] - sm_clock[i] <= 3 * max_drift);


  sm_cm_clock_distance_strict: LEMMA
     TTE |- G(FORALL (i: SM_ID, j: CM_ID):
                  sm_clock[i] - cm_clock[j] < 3 * max_drift AND 
                  cm_clock[j] - sm_clock[i] < 3 * max_drift);

END