Algorithms and Tools for the Automatic Analysis of Embedded Systems

摘要

Over the duration of the award, we developed formal methods and tools for the design, verification, and control of embedded systems. This was accomplished by extending techniques, based on automata theory and temporal logic, from the analysis of time-independent reactive systems to real-time embedded systems. As system specification language for embedded systems, we introduced hybrid automata, which equip traditional discrete automata with real- numbered clock variables and continuous environment variables. As requirements specification, we introduced temporal logics with clock variables for expressing timing constraints.