See this page for help with
installing and running tools
[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.
[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.
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.