BLESS Specification
BLESS allows formal specification of embedded system behavior designed with the Architecture Analysis and Design Language (AADL).
BLESS Behavior
BLESS programs behavior of AADL components using state-transition machines.
BLESS Editor and Proof Assistant
BLESS has plugins to Open Source AADL Tool Environment (OSATE) for editing, and formal verification that behavior conforms to its specification