NSF: Verification of Open-Loop Embedded Control Systems

This project develops automated techniques for efficiently analyzing the correctness of open-loop embedded control software. Such software is widespread in the real-world, in automotive, flight-control, medical-device and other human-in-the-loop applications, where environmental behavior is unpredictable. The research effort is based on the observation that such software can be effectively modeled using a particular mathematical formalism called timed automata. The specific topics being studied include: 1) Model checking: novel on-the-fly algorithms, in which system behavior is explored in a demand-driven manner, are being developed for checking properties of timed automata. 2) Industry-standard modeling and model checking: strategies are being devised for adapting the model-checking tools to industry-standard modeling notations such as Simulink© and for exploiting model structure to enable verification of large models that arise in practice. The significance and impact of the work derive from the more thorough verification of control software the new technologies will enable. By automating formal validation activities and supporting widely used modeling tools, the research will empower engineers to conduct more intensive analyses of their control-system designs earlier in the life-cycle than current techniques allow.

Verification of Open-Loop Embedded Control Systems is a four-year, $350K grant.