Describir: MODEL-BASED VERIFICATION OF EMBEDDED SOFTWARE.