Algorithms and Tools for the Automatic Analysis of Embedded Systems
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 06, 1998
- Accession Number
- ADA350960
Entities
People
- Thomas Henzinger
Organizations
- University of California, Berkeley