BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software NFM 2013