Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

Quelle physical_clocks.pvs Sprache: PVS

%
% Purpose      : This theory provides the basic definitions and
%                properties concerning  the relative drift of good
%                oscillators.  The drift bounds for a good oscillator
%                are captured in the declared type `good_clock'.
%                A good_clock is a function from Clocktime (integer) to
%                realtime (real) with a bounded rate of drift.
%
% Assumptions  : Oscillators have a bounded rate of drift with respect
%                to (Newtonian) real time.  This bound is captured by
%                formal parameter rho.
%

physical_clocks
[
   rho : nonneg_real
] : THEORY

  BEGIN

  IMPORTING
     abs_props, floor_ceiling_ineq

% First define drift in terms of rho so that that we can use simpler
% terms for bounding relative drift.

  rate: posreal = 1 + rho
  drift: nonneg_real = rate - 1 / rate
  drift_def: LEMMA drift = (rate * rate - 1) / rate
  drift_bound: LEMMA drift <= 2 * rho

% Various variable declarations

  X: VAR nat
  T, T1, T2: VAR int
  t: VAR real
  clock: VAR [int -> real]
  skew : VAR nnreal
  adj: VAR real

% TYPE good_clock formalizes the notion of oscillator drift within
% some bound, rho.  In essence, a good oscillator is characterized by
% the behavior of an (imaginary) unbounded counter.

  good_clock: NONEMPTY_TYPE =
    { clock |
         FORALL T:
           1 / rate <= clock(T + 1) - clock(T) AND
                       clock(T + 1) - clock(T) <= rate
    } CONTAINING LAMBDA T: T

  c, c1, c2: VAR good_clock

  clock_edge?(c, t): bool = EXISTS T: t = c(T)

  drift_left_nat: LEMMA
    X / rate <= c(T + X) - c(T)

  drift_right_nat: LEMMA
    c(T + X) - c(T) <= X * rate

  drift_left: LEMMA
      T1 <= T2 IMPLIES
        (T2 - T1) / rate <= c(T2) - c(T1)

  drift_right: LEMMA
      T1 <= T2 IMPLIES
        c(T2) - c(T1) <= (T2 - T1) * rate

  abs_drift_lb: LEMMA
      abs(T1 - T2) / rate <= abs(c(T1) - c(T2))

  clock_nondecreasing: LEMMA
       T1 <= T2 IMPLIES c(T1) <= c(T2)

  clock_increasing: LEMMA
       T1 < T2 IMPLIES c(T1) < c(T2)

  clock_nondecreasing_alt: LEMMA
       c(T1) <= c(T2) IMPLIES T1 <= T2

  clock_eq_arg: LEMMA
       c(T1) = c(T2) IMPLIES T1 = T2

  offset_clocks?(c1, c2): bool =
    EXISTS T2: FORALL T1: c1(T1) = c2(T1 + T2)

  relative_drift: LEMMA
    c1(T1 + X) - c2(T2 + X) <= c1(T1) - c2(T2) + drift * X

  nonoverlap_basis: LEMMA
    c1(T) - c2(T) <= adj AND
    T2 - T1 > rate * adj AND
    T1 <= T AND
    T <= T2
  IMPLIES
    c1(T1) < c2(T2)

  skew_basis_0: LEMMA
    c1(T) - c2(T) <= adj AND
    c2(T2) < c1(T1) AND
    T1 <= T AND
    T <= T2
  IMPLIES
    T2 - T1 < rate * adj

  skew_bound_1: LEMMA
    c1(T) - c2(T) <= skew AND
    c2(T2) <= c1(T1)  AND
    T1 <= T + X AND
    T - X <= T2
  IMPLIES
    T2 - T1 <= rate * (skew + drift * X)

  skew_bound_2: LEMMA
    c1(T) - c2(T) <= skew AND
    c2(T2) < c1(T1)  AND
    T1 <= T + X AND
    T - X <= T2
  IMPLIES
    T2 - T1 < rate * (skew + drift * X)

% basis of skew_conversion_sym in inverse_clocks:

  skew_bound: LEMMA
      abs(c1(T) - c2(T)) <= skew AND
      abs(T2 - T) <= X AND
      c1(T1) <= c2(T2) AND
      c2(T2) < c1(T1 + 1)
    IMPLIES
      abs(T1 - T2) <= ceiling(rate * (skew + drift * X))

% offset properties for accuracy

  lower_offset: LEMMA
      T1 - X <= T2
    IMPLIES
      T2 - T1 <= rate * (c(T2) - c(T1) + drift * X)

  upper_offset: LEMMA
      T1 - X <= T2
    IMPLIES
      (c(T2) - c(T1) - drift * X) / rate <= T2 - T1

  END physical_clocks

quality91%

¤ Dauer der Verarbeitung: 0.12 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.