BLESS: Behavior Language for Embedded Systems with Software

BLESS is a verification language for writing correctness proofs, as well as a tool for executing those proofs.

It functions as an annex to the Architecture Analysis and Design Language (AADL) to provide capability for adding provably correct behavior to models of embedded, software executing, electronic systems.

Syndicate content