Embedded systems and cyber-physical
systems (CPS), combine software components with sensors,
actuators & communication. From smart driver-assist systems, to air-traffic control
systems, many next-generation engineering systems are exampled of CPS.
While this synergy of computation and control has led to the creation of many new
products and services (for example, Kiva Systems),
it also makes their design and analysis a challenge.
In this course you will:
(a) Learn to model and analyze
CPS systems
(b) Use powerful software tools (model
checkers, SMT solvers,
& theorem
provers) for designing & analyzing systems
(c) Read and discuss recent ideas from
research papers
The course meets twice a week, has 4-5 home works,
and a semester-long project. All reading material will be
available here. Projects typically lead to conference papers. We
will provide some project ideas, but you are also welcome to
design a project around your own research. Examples:
o Building/verifying a system with Android
phones & mobile robots
o Building a verification technique/tool and
trying it on benchmarks
o Case studies on new CPS
Tentative topics: • Review of Automata, languages,
invariant proofs, linear systems, and stability • Models for
discrete time, synchronous, and asynchronous, distributed
systems • Temporal logics and model checking • Real-time and
hybrid system models, stability verification: Multiple Lyapunov
functions, slow switching, dwell time, abstractions,
bisimulation and simulation • Abstraction and refinement •
Undecidability and limits of algorithmic analysis and
verification • Deductive verification with mechanical theorem
provers • Applications to clock synchronization, path planning
in robotics, supervisory control, biology •