| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle synch_constant_definitions.pvs Sprache: PVS |
|||||||||
|
%
% Purpose : Definitions of various period related constants, % based on paramters derived from the synchronization % protocol. % % P - nominal duration (in ticks) between % resynchronization events. % rho - bound on drift for a good oscillator % alpha_l - lower bound on loss of accuracy due to % computing and applying adjustment (may be 0). % alpha_u - upper bound on loss of accuracy due to % computing and applying adjustment (may be 0). % pi_0 - intantaneous precision bound immediately % after applying computed adjustment (> 1) % synch_constant_definitions [(IMPORTING synch_parameter_constraints) P: posnat, T0: int, rho: nnreal, alpha_l, alpha_u: nnreal, pi_0: {pi : posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)} ]: THEORY BEGIN IMPORTING physical_clocks[rho] % for definition of rate, drift j, k: VAR nat P_bound: LEMMA rate * (pi_0 + max(alpha_l, alpha_u) + drift * P) < P rho_bound: LEMMA rho * (2 + rho) < 1 %%% NOT USED ADJ: nat = floor(rate * (pi_0 + max(alpha_l, alpha_u) + drift * P)) ADJ_ineq: LEMMA ADJ >= floor((drift * P + pi_0) * rate) ADJ_ineq_l: LEMMA ADJ >= floor((drift * P + alpha_l + pi_0) * rate) ADJ_ineq_h: LEMMA ADJ >= floor((drift * P + alpha_u + pi_0) * rate) ADJ_bound: LEMMA ADJ < P P_min: posnat = P - ADJ %%% NOT USED P_max: posnat = P + ADJ p_min_bound: LEMMA rate * (pi_0 + max(alpha_l, alpha_u)) < P p_lower: posreal = P / rate - alpha_l p_upper: posreal = P * rate + alpha_u p_min: posreal = P / rate - alpha_l - pi_0 p_max: posreal = P * rate + alpha_u + pi_0 p_min_lower: LEMMA p_min = p_lower - pi_0 p_max_upper: LEMMA p_max = p_upper + pi_0 drift_P_bound: LEMMA drift * P < p_min Pi: posnat = ceiling(rate * (max(alpha_l, alpha_u) + pi_0 + drift * (P_max + 1))) END synch_constant_definitions ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28