Why Model-based Programming MERS Polar Lander Leading Diagnosis Legs deployed during descent Noise spike on leg sensors latched by software monitors Laser altimeter registers 40m Begins polling leg monitors to determine touch down Read latched noise spike as Objective: Support programmers touchdown with embedded languages that Engine shutdown at -40m avoid these mistakes, by reasoning about hidden state Programmers often make automatically commonsense mistakes when Reactive Model-based reasoning about hidden state Programming Language(RMPL)Why Model-based Programming? Polar Lander Leading Diagnosis: • Legs deployed during descent. • Noise spike on leg sensors latched by software monitors. • Laser altimeter registers 40m. • Begins polling leg monitors to determine touch down. • Read latched noise spike as touchdown. • Engine shutdown at ~40m. Programmers often make commonsense mistakes when reasoning about hidden state. Objective: Support programmers with embedded languages that avoid these mistakes, by reasoning about hidden state automatically. Reactive Model-based Programming Language (RMPL)