# 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.