From AadlWiki

Jump to: navigation, search

The Behavior Language for Embedded Systems with Software is an extension of the behavior modeling language BA to be a complete programming language including type system and formal semantics. When behavior is annotated with assertion to be a proof outline, a proof tool can transofrm the proof outline (with human selection of tactics) into a complete, formal proof that every execution meets its specification. Language reference manual (LRM), example models, and an OSATE plugin featuring Xtext-based editor for BLESS annex subclauses and the proof tool are available at

Personal tools