Fall2014

ECE/CS 584: Embedded & Cyberphysical System Verification

What? Embedded systems and cyber-physical systems (CPS), combine software components with sensors, actuators & communication. Look inside the electronic controllers in your car, in smart meters, in air-traffic control systems and you will most likely find a CPS of some flavor. While this synergy enables the materialization of brand new ideas (For example, Kiva Systems), it also makes their design and analysis much more challenging.

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

How? 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 •