Problem Sets



People Involved

Sayan Mitra, Lecturer
mitras at illinois.edu
Phone: 333-7824
Office: CSL 226

Spring 2016

ECE/CS 584: Embedded & Cyberphysical System Verification


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 •