An adequate level of safety and reliability for embedded systems can be guaranteed only through the use of computer aided design and analysis tools in the development process. This research investigates several key questions whose solution is expected to increase the scope and decrease the cost of symbolic analysis techniques for embedded systems. Simultaneously, the project is implementing the new algorithms and strategies for the automatic analysis of embedded systems within the prototype tool HyTech that is being developed at Cornell. Embedded systems are modeled as Hybrid Automata, which combine discrete system transitions and continuous environment activities. Symbolic model checking and abstract interpretation are used to automatically compute the conditions under which a hybrid automaton satisfies a temporal-logic requirement. The method has been implemented in HyTech, which allows the automatic analysis of hybrid automata with piecewise-linear behavior. The purpose of this work is, first, to improve the applicability and the efficiency of HyTech and, second, to investigate--through theory, implementation, and case studies--how far standard program-analysis methods can be generalized to permit the direct analysis of continuous-time systems.
