BLESS: Behavior Language for Embedded Systems with Software

BLESS is an annex sublanguage of the Architecture Analysis and Design Language (AADL) to define and specify real-time, reactive behavior of embedded systems.

The goal of the BLESS language is to enable the construction of proofs for AADL models that their (operational) behavior upholds their (declarative) specification. Therefore all specifications, programs, and executions be precise, mathematical objects, about which propositions can be made, and proven correct.

BLESS annex subclauses of AADL components define behavior with state-transition machines. Transitions between states have a condition which must be met before the transition can be taken, and possibly an action before entering a destination state.

BLESS assertions are temporal logic formulas which are used for both declarative behavior specification, and for annotation of state-transition machines. Specifications of an AADL component attaches BLESS::Assertion properties to features (usually ports, but parameters for subprogram components), and a BLESS::Invariant property to the component itself. Assertions annotating imperative behavior of BLESS annex subclauses form a proof outline that can be transformed into an inductive proof with the BLESS proof tool.