Quelle virtual_clock_2.pvs Sprache: PVS

%
% 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 second scenario and shows that is satisfies the
%                precision  and accuracy requirement of clock
%                synchronization.
%
virtual_clock_2
[(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
  ac, ac1, ac2: VAR weakly_accurate_clock
  t1: VAR real
  j: VAR nat

  % required properties of t(ac) event_sequence

  t_increasing: LEMMA increasing?(t(ac))
  t_unbounded: LEMMA unbounded?(t(ac))
  t_event_sequence: JUDGEMENT t(ac) HAS_TYPE event_sequence

  t_nonoverlap: LEMMA
      compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u))
    IMPLIES
      nonoverlap?(t(ac1), t(ac2))

  t_early: LEMMA earliest_adjustment?(ac, 0)(t(ac))
  t_self: LEMMA self_adjustment?(ac, ADJ + 1)(t(ac))
  t_cross: LEMMA
      compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u))
    IMPLIES
      cross_adjustment?(ac1, ADJ + 1)(t(ac2))

  % main results

  VC2(ac)(t1): int = VC(t(ac))(ac)(t1)

  VC_j: LEMMA VC2(ac)(t(ac)(j)) = T(j)

  VC2_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(VC2(ic1)(t1) - VC2(ic2)(t1)) <= Pi

  VC2_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)) / rate
          < 1 + VC2(ic)(t1) - T(0)

  VC2_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
          < 1 + VC2(ic)(t1) - T(0)

  VC2_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
      VC2(ic)(t1) - T(0)
         <= ((t1 - t(ic)(0)) * (1 + alpha_l / p_lower)
              + pi_0 * (1 + alpha_l / p_lower)) * rate

  VC2_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
      VC2(ic)(t1) - T(0)
         <= ((t1 - t(ic)(0)) + pi_0) * rate

END virtual_clock_2

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.