|
%
%
% Purpose: The protocol (relationship between what is received and
% what is sent) when the message datatype is used with
% the integration fault model.
%
%
protocol_integration
[
N: [nat -> posnat],
T: TYPE+
] : THEORY
BEGIN
i, j, k: VAR nat
element: T % to eliminate TCC's
IMPORTING
comm_integration[N, T],
protocol[N, message[T]]
status: VAR [i: nat -> node_status[N(i)]]
sent: VAR [i: nat -> [below(N(i)) -> message[T]]]
common_check: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
msg_check: VAR valid_check_function
check: VAR check_function
vf: VAR choice_function
% cf: VAR compute_function
protocol(sent, check, vf, status, j, k): bool =
protocol(vf, sent, rcvd(sent, status), check, j, k)
% protocol(sent, check, vf, cf, status, j, k): bool =
% protocol(cf, vf, sent, rcvd(sent, status), check, j, k)
END protocol_integration
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
