曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
dependencies, as well as specifying state changes, thus ensuring that Boolean
logic must be supplemented by a semantics that considers change over time,
hence our preference for TLA. In the semantics of TLA, a collection of Boolean
values of the propositions describes a state. A proposition is a state predicate,
since its Boolean value depends on the state in which it is evaluated. A logical
formula describing how a state changes is called an action.
4
Real-time constraints also appear essentially in the FCOM description, e.g.:
The system is disarmed by: [...] flight condition since 10 seconds. Ground
spoilers retraction is achieved when: [...] at least 3 sec between 4◦ and 20◦.
They may be handled in TLA [AL94], but we don’t attempt that here. In
[Lad95], we identified the following problems with the descriptions:
ambiguities due to imprecise statement, or to infelicitous phrasing in English;
confusion between action and state: a desired result is achieved when, e.g. [X]
occurs when [Y] is activated, or [X] occurs when lever [Y] is pulled up. Do
the conditions on [Y] refer to its state, or to an action performed on [Y]?
Whether certain states are acceptable or anomalous may depend on which
reading is given;
imprecision in stating Boolean conditions: potentially ambiguous English de-
scriptions are used to represent Boolean expressions, especially since paren-
theses are not included. However, in at least one place, an accurate
Boolean formula is used. Pilots are clearly expected to understand Boolean
formulas;
multiple terms used for a single concept or value: for example insufficient
pressure, or low pressure; such terms are rarely noted to be synonyms;
incorrect mathematics is used in one place to describe a crucial quantity–an
integral should be used, but does not appear.
4 The FCOM Specification as Predicate-Action
Diagrams
We use predicate-action diagrams to represent the information contained in
the specification. Predicate-action diagrams are almost self-explanatory. The
nodes are partial states, that is they are collections of values of selected state
predicates. We call these partial states ‘states’. ‘Actions’ change the values of
the state predicates, and are represented by arrows between the ‘states’. The
‘actions’ represented in the diagrams are collections of all the actions that can
change the value of one of the predicates of the ‘state’. It is required that the
result of any action that changes the value of the ‘state’ belongs to one of the
‘actions’, and that all the ‘states’ that result from any of the actions belonging
to an ‘action’ appear in the diagram. Thus, a predicate-action diagram focuses
on certain predicates, and shows how the values of those state predicates are
changed by actions of the system, which are grouped into sets of actions that
all have the same effect on the selected state predicates.
In the representation of the FCOM specification in predicate-action dia-
grams, we represent the ‘actions’ by logical disjunctions of its component ac-
tions. We also label the ‘states’ by certain useful indicative expressions. Thus,
a braking-mode ‘state’ labelled with normal satisfies the state predicate that
braking-mode = normal. However, these labels, while helpful, do not neces-
sarily correspond to explicit state predicates. The state predicates explicitly
asserted in the ‘state’ are given by conjunctions written in an ellipse attached
by a line to the ‘state’.
5
(green lowpress AND yellow lowpress)
BSCU failure OR
Alt with A/S Alt w’out A/S
Normal
Autobrake available
Antiskid operative AND
Prkbrk off AND
A/S on AND N/W STRG on AND
green press ‘avail’ AND
Autobrake inoperative
Antiskid operative AND
Prkbrk off AND
yellow lowpress
green lowpress
A/S on AND N/W STRG on AND
yellow press ‘avail’ AND
power supply failure OR
(A/S off AND N/W STRG off) OR
[(A/S off AND n/W STRG off) OR
power supply failure OR
(green lowpress AND yellow lowpress)] AND
BSCU failure OR
Autobrake inoperative
Figure 1: The Braking Modes from the FCOM Specification
Parkbrake
Antiskid off
Alternate w’ antiskid OR
Normal OR
Alternate w’out antiskid
‘Operate’ PBr handle
Figure 2: The Parking Brake Mode from the FCOM Specification
We omit the predicate-action diagram corresponding to the thrust reverser
system, because it is not revised when we apply our rewriting criteria.
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料12(9)
