Software Tools

- UPPAAL : A model checker for timed systems.
- PVS : A general-purpose theorem prover for higher order logic.
- PHAVER: A model checker for Hybrid Systems
- SpaceEx:
Another model checker for Hybrid Systems

- Tempo : A GUI-based tool for developing TIOA/HIOA specifications and translating specifications to UPPAAL and PVS.

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.

Miscellaneous

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.