Oct. 12th and 26th, 1999: SEC Study Group: Timed Automata Verification

Study materials

Main material

A very good introductory survey for timed-automata is:
- R. Alur. etc. "Timed Automata". NATO-ASI 1998 Summer School on Verification of Digital and Hybrid Systems.
More publications of Rajeev Alur on timed-verification can be found in his home page: http://www.cis.upenn.edu/~alur/onlinepub.html
Since this group is particularly interested in modeling and analyzing scheduling applications with timed automata, the following two papers might be of interest:
- S. Bornot, J. Sifakis, and S. Tripakis "Modeling Urgency in Timed Systems" in Compositionality: the significant difference, COMPOS'97, Springer LNCS 1536. (pdf version)
- K. Altisen, etc. "A Framework for Scheduler Synthesis" (pdf verison)
Finally, the following paper contains a detailed view of recent work on compositionality for timed systems.
- S. Bornot and J. Sifakis, "An Algebraic Framework for Urgency" to appear in Information and Computation, special issue on compositionality. (pdf version)
S. Bornot, G. Gobler, and J. Sifakis, "On the Construction of Live Timed Systems" Submitted to TACAS 2000. ( pdf version)

Other resources

General context: formal methods, and more precisely, verification/controller synthesis/test generation for real-time systems.
Brief history:
Books: none on timed-automata in particular, many on verification (using different models). Manna/Pnueli is classic, Alur/Henzinger is being written, Clarke/Grunberg/McMillan are also writing one on model-checking. Also, "Design and Validation of Computer Protocols", by G.Holzmann (author of Spin).
Papers: many...
I suggest that you read the survey paper by Alur above. This paper contains many interesting references.
The papers involving me as an author are available on my web-page.
My web-page: http://www-verimag.imag.fr/PEOPLE/tripakis/
Some of my presentations:
Verification tools:
- Kronos
- Uppaal
- lDT-Spin
- Other verification tools not specialized to timed-automata:
  - Spin
  - SMV
  - Mocha
  - SMI
Formal Methods Conferences