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.

Syndicate content