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


Software Tools

See this page for help with installing and running tools

Recommended Reading

[MSip96] Michael Sipser. Introduction to Theory of Computation International Thomson Publishing, 396 pages, 1996.

[TIOA06] Dilsun Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. The Theory of Timed I/O Automata, Morgan & Claypool, 2006.

[CGP00] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.

[MMuk96] Madhavan Mukund. Finite-State Automata on Infinite Inputs. A tutorial, 1996. (We will not cover Section 2)

[ORR+96] S. Owre, S. Rajan, J. M. Rushby, N. Shankar and M. Srivas. PVS: Combining specification, proof checking, and model checking. CAV'96, pages 411--414, Springer-Verlag, 1996.

[HK02] Henzinger and Kirsch. Embedded Machine: Predictable, portable, real-time code. PLDI 2002, ACM press.

[HHK01] Henzinger, Horowitz, and Kirsch. Giotto: A time-triggered language for embedded programming. In Proceedings of the IEEE, pages 166–184. Springer-Verlag, 2001.

[Henz95] Thomas Henzinger, Peter Kopke, Anuj Puri, and Pravin Varaiya. What's Decidable About Hybrid Automata?. Journal of Computer and System Sciences, pages 373–382. ACM Press, 1995.

[ACH+95] Rajeev Alur et al. The Algorithmic Analysis ofHybrid Systems. Theoretical Computer Science, colume 138, pages 3-34, 1995.

[BDL04] Gerd Behrmann, Re David, and Kim G. Larsen. A tutorial on UPPAAL. In Proc. Formal Methods for the Design of Real-Time Systems (SFM-RT 2004), volume 3185 of LNCS, pages 200–236. Springer, 2004.

[LSV03] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Hybrid I/O automata. Information and Computation, 185(1):105-157, August 2003.

[LT89] Nancy Lynch and Mark Tuttle. An introduction to Input/Output automata. CWI-Quarterly, 2(3):219-246, 1989.

[Lee08] Edward A. Lee. Cyber physical systems: Design challenges. In International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), May 2008. Invited Paper.

[Hen07] Tom Henzinger. Reliable Systems Engineering. Inaugural lecture at EPFL, 2007.

[DL03] Daniel Liberzon. Switching in Systems and Control. Birkhauser, 2003.

Additional References

[BLL+96] Johan Bengtsson, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. UPPAAL in 1995. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 431–434, 1996.

[BK08] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

This excerpt explains the relationship amongst the different hybrid and timed automata models, and the chronology of their development.

[MMT91] Michael Merritt, Francesmary Modugno, and Mark Tuttle. Time constrained automata. 2nd International Conference of Concurrency Theory, volume 527, pages 408-423, 1991.

[Hen96] Thomas A. Henzinger. The theory of hybrid automata. In 11th Annual IEEE Symposium on Logic in Computer Science, pages 278-292, 1996.

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.

[MS00] Olaf Müller and Thomas Stauner. Modelling and verification using linear hybrid automata-a case study. Mathematical and Computer Modelling of Dynamical Systems, 6(1):71-89,2000.

Class Project Publications

The following is an incomplete list of publications are related to past projects done by students in this class.

[HM12] Zhenqi Huang and Sayan Mitra:Computing bounded reach sets from sampled simulation traces. HSCC 2012: 291-294.

[Zim12] Adam Zimmerman. SrarL for programming reliable robotic netwroks. Masters Thesis. UIUC, 2012.

[MMBC11] Karthik Manamcheri, Sayan Mitra, Stanley Bak, Marco Caccamo: A step towards verification and synthesis from simulink/stateflow models. HSCC 2011: 317-318.

[HDJ13] Hossain, Dhople, and Johnson. Reachability analysis of closed-loop switching power converters. Power and Energy Conference at Illinois (PECI), 2013 IEEE, 130-134.


Latex prelude for lecture notes.
Bibliography for lecture notes (rename this file to hyb_course.bib).

PVS Language Reference describes the syntax and semantics of PVS language.
PVS System describes the user interface including with a quick guide.
PVS Prover Guide is the complete reference for PVS proof commands.
NASA Langley PVS course.

UPPAAL tutorial talk presents a quick overview and this paper discusses the tool in detail.
Another UPPAAL tutorial paper.
Several UPPAAL case studies presented by Radek Pelanek.

Wikipedia page on Lego Mindstorms NXT with many links to tools and programming languages.
Lego advanced Open Source NXT Firmware, docs for NXT virtual machine, SDK.
NXT executable file format doc.
NXT hardware: basic architecture, sensors docs.