Home
Administrivia
Overview
Schedule
Problem Sets
Resources
For many engineering systems, correctness depends critically on the interactions between software components and their physical environment. Think of mobile robots, air-traffic control systems, vehicle control systems, real-time distributed systems. The hybrid system formalism, which combines automata with differential equations, has emerged as a compelling way of modeling and analyzing such systems. This formalism has been used to model, verify, and synthesize a wide variety of systems including those mentioned above.
This course is an introduction to the field of hybrid systems with emphasis on specification and verification. We will start with automata-based models for describing discrete time distributed systems, then we will introduce simple continuous dynamics, and move to hybrid automata with more general dynamics. The course will provide an overview of tools and techniques that are available for verifying different classes of hybrid automata models. A significant component of the course is the semester-long project. Projects may involve building and verifying a "real" system, developing software tools, or developing theoretical models and techniques for verification. While some project ideas and related hardware/software packages will be provided, you are also welcome to find a suitable project topic from your own research.