BLESS specifications of AADL component behaviors consist of properties of component features, usually ports. These properties are predicates (a.k.a. assertions) stating what is assumed to be true about received values on that feature, or guaranteed to be true about values sent. In addition, components may have an invariant which is (supposed to be) always true.
BLESS predicates are first-order predicates, augmented with simple temporal operators that say when a predicate should be evaluated. First-order predicates are basically boolean-valued expressions with the addition of quantifiers like for-all (∀) and there-exists (∃). If
p is a predicate and
t is a time, then
p@t means to evaluate predicate
p at time
BLESS predicates are delimited by double angle brackets
<< >>. This is a predicate that says when a pacemaker should apply a pacing pulse of current:
This defines a predicate,
VP, which is true when the pacemaker should deliver a pulse of electricity (about 2 Volts for half a millisecond). VP is used to specify the behavior of an AADL thread which controls “VVI” mode pacing.
VVI issues an event on port
p, it guarantees that
VP() is true. In addition to predicates on ports
n, the specification of
VVI includes an invariant predicate
LRL(now). The whole thread specification and implementation can be found in VVI.aadl.