曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
s1 -[ RESUME ]-> s0;
END ANNEX cotre.behavior;
General behavioral description (thread case):
ã AIRBUS France / IRIT / LAAS / ONERA/CT-DTIM / GET-Ecole Nationale Supérieure des Télécommunications de Bretagne / TNI-Valiosys - 2004
F241-2 Page 14/45
ANNEX cotre.behavior IS
STATES
s0, s1, s2, s3, s4, s5, s6, s7, s8 : STATE;
s0 : INITIAL STATE;
TRANSITIONS
s0 -[ ]-> s1 { PERIODIC_WAIT };
s1 -[ ]-> s2 { COMPUTATION(1.9ms, 1.9ms) };
s2 -[ s1.wait ! (-1.0ms) ]-> s3;
s3 -[ ]-> s4 { COMPUTATION(0.1ms, 0.1ms) };
t1: s4 -[ s2.wait ! (-1.0ms) ]-> s5;
s5 -[ ]-> s6 { COMPUTATION(2.5ms, 2.5ms) };
t5: s6 -[ s2.release ! ]-> s7;
s7 -[ ]-> s8 { COMPUTATION(1.5ms, 1.5ms) };
s8 -[ s1.release !]-> s9;
END ANNEX cotre.behavior;
4.5 Expression of contracts
COTRE contracts can express obligations and guarantees, in the form of assertions or
behavioral equivalences.
4.5.1 Assertions
The following assertions are supported:
Assertion Formal Description Comment
potentially reset AG EF init The component can return to its inital
state from any other state.
unavoidably reset AG AF init The component must return to its inital
state from any other state.
is alive AG EF EXctrue Component actions must always be possible
in the future. Applied to a root component,
this assertion implies absence of
inter-blocking.
no livelock AG AF EXctrue The component must not remain inactive
indefinitely.
invariant <exp> AG <exp> <exp> must always be true.
<exp1> leads to <exp2> [within
<exp3>]
AG(e1=>AF<=d e2) The occurrence of <exp1> always leads
to the occurrence of <exp2> within a period
of time less than <exp3>.
reachable <exp1> [from <exp2>]
[within <exp3>]
AG(e1=>EF<=d e2) The occurrence of <exp1> may lead to
the occurrence of <exp2> within a period
of time less than <exp3>.
<exp1> after <exp2> AG(¬EU(¬e2, e1)) The occurrence of <exp1> is always preceded
by the occurrence of <exp2>.
4.5.2 Behaviors
A component’s abstract behavior can also be described by an automaton specifying the
constraints – sequence, non-determinism, parallelism, conflict, etc. – between the dfferent
actions (not necessarily all of them) to be observed.
The check then consists of ensuring that there is equivalence between the abstract behavior
and the real behaviour. Several behavioral equivalences, offering increasing discrimination
power, are considered:
ã AIRBUS France / IRIT / LAAS / ONERA/CT-DTIM / GET-Ecole Nationale Supérieure des Télécommunications de Bretagne / TNI-Valiosys - 2004
F241-2 Page 15/45
Convention Comment
language Ensures that the executions that can be observed from the abstract & real
behaviors are identical. Does not take into account either the possibility of
blocking (state in which no action can be observed) or the possibility of divergence
(infinite execution involving only non-observable actions).
observational In addition to language equivalence, takes into account blocking states and
the conservation of non-determinism. Divergent executions are ignored.
branching In addition to observational equivalence, takes into account divergent executions.
The associated syntax is as follows:
…
BEHAVIOR (<convention> equivalence)
STATES
<nom état>(, <nom état>)* : STATE;
<nom état> : INITIAL STATE;
TRANSITIONS
<transition 1>;
<transition 2>;
…
<transition n>;
END;
…
4.5.3 Environmental constraints
Use the appendix cotre.assumes if you want a component to ask its environment to
conform to certain constraints.
4.5.4 Operating guarantees
A component announce the properties it guarantees using the appendix cotre.guarantees.
4.6 COTRE-specific property sets
As shown in the table below, analysis of the attributes identified in the COTRE metamodel
and those of the AADL language has revealed a certain number of points which
are not covered.
ã AIRBUS France / IRIT / LAAS / ONERA/CT-DTIM / GET-Ecole Nationale Supérieure des Télécommunications de Bretagne / TNI-Valiosys - 2004
F241-2 Page 16/45
COTRE Type COTRE AADL Type AADL Notes
Application:name String Nom composant string
Component:actif Boolean thread
Component:description String - - Documentary role
Component:generic Boolean - Concept not supported by AADL
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料4(119)
