products/Sources/formale Sprachen/PVS/analysis_ax/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: virtual_clock_1.pvs   Sprache: Unknown

%
% Purpose      : There are two common scenarios for synchronization
%                protocols to apply instantaneous adjustments.  The
%                first is to compute a correction term for the current
%                interval,and apply the correction when the Clocktime
%                reaches a specific value.  The second is to set the
%                local counter to a specific value in response to some event.
%                This file presents a virtual clock based upon the first
%                scenario and shows that is satisfies the Precision
%                requirement of clock synchronization 
%

virtual_clock_1
[(IMPORTING synch_protocol_invariants)
    P: posnat,     % Nominal duration of a synchronization interval
    T0: int,       % Clocktime at start of protocol
    rho: nnreal,   % Bound on drift for a good oscillator
    alpha_l, alpha_u: nnreal,  % negative and positive read error bounds
    pi_0: {pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}
] : THEORY

  BEGIN

  IMPORTING 
    synch_protocol_invariants[P, T0, rho, alpha_l, alpha_u, pi_0],
    virtual_clocks[P, T0, rho]


  hst: VAR [nat -> non_empty_finite_set[good_clock]]
  ic, ic1, ic2: VAR interval_clock
  t1: VAR real

  ac, ac1, ac2: VAR weakly_accurate_clock
  k : VAR nat
  j: VAR posint

  % Definition and required properties of turns(ac) event_sequence

  turns(ac)(k): real = IF k = 0 THEN ac(0)(T(0)) ELSE ac(k-1)(T(k)) ENDIF

  turns_increasing: LEMMA increasing?(turns(ac))
  turns_unbounded: LEMMA unbounded?(turns(ac))
  turns_event_sequence: JUDGEMENT turns(ac) HAS_TYPE event_sequence

  turns_nonoverlap: LEMMA
      compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u)) AND
      compatible?(ac2, ac1, pi_0 + max(alpha_l, alpha_u))
    IMPLIES
      nonoverlap?(turns(ac1), turns(ac2))
  
  turns_early: LEMMA earliest_adjustment?(ac, ADJ + 1)(turns(ac))
  turns_self: LEMMA self_adjustment?(ac, ADJ + 1)(turns(ac))
  turns_cross: LEMMA
       compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u)) AND
       compatible?(ac2, ac1, pi_0 + max(alpha_l, alpha_u))
    IMPLIES
      cross_adjustment?(ac1, ADJ + 1)(turns(ac2))

  % main results

  VC1(ac)(t1): int = VC(turns(ac))(ac)(t1)

  VC1_j: LEMMA VC1(ac)(turns(ac)(j)) = C(ac(j))(ac(j - 1)(T(j)))

  VC1_precision: THEOREM
      trace?(ic1, hst) AND
      trace?(ic2, hst) AND
      initial_precision?(hst, pi_0) AND
      synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
      max(t(ic1)(0),t(ic2)(0)) <= t1
    IMPLIES
      abs(VC1(ic1)(t1) - VC1(ic2)(t1)) <= Pi

  VC1_accuracy_lower: THEOREM
      trace?(ic, hst) AND
      initial_precision?(hst, pi_0) AND
      synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
      t(ic)(0) <= t1
    IMPLIES 
      ((t1 - t(ic)(0)) *  (1 - (alpha_u / p_lower)) 
        - pi_0 * (1 + alpha_u / p_lower)
        - (drift + rate * (alpha_u / p_lower)) * (1 + ADJ)) / rate
          < 1 + VC1(ic)(t1) - T(0)

  VC1_optimal_accuracy_lower: COROLLARY
      alpha_u = 0 AND
      trace?(ic, hst) AND
      initial_precision?(hst, pi_0) AND
      synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
      t(ic)(0) <= t1
    IMPLIES 
      ((t1 - t(ic)(0)) - pi_0) / rate 
          - drift * (1 + ADJ) / rate
                < 1 + VC1(ic)(t1) - T(0)

  VC1_accuracy_upper: THEOREM
      trace?(ic, hst) AND
      initial_precision?(hst, pi_0) AND
      synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
      t(ic)(0) <= t1
    IMPLIES 
      VC1(ic)(t1) - T(0) 
         <= ((t1 - t(ic)(0)) * (1 + alpha_l / p_lower) 
             + pi_0 * (1 + alpha_l / p_lower)) * rate
             + (1 + ADJ) * (drift + rate * alpha_l / p_lower) * rate

  VC1_optimal_accuracy_upper: COROLLARY
      alpha_l = 0 AND
      trace?(ic, hst) AND
      initial_precision?(hst, pi_0) AND
      synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
      t(ic)(0) <= t1
    IMPLIES 
      VC1(ic)(t1) - T(0) 
         <= ((t1 - t(ic)(0)) + pi_0) * rate
              + (1 + ADJ) * drift * rate

  END virtual_clock_1

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]