SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Tempo: A Model Checker for Event-Recording Automata
 by Maria Sorea.

Abstract
We present a symbolic on-the-fly model checking algorithm for event-recording automata, a subclass of timed automata. This algorithm is based on a forward reachability analysis and uses a symbolic representation of clock constraints. It forms the core of the verification tool TEMPO. We also develop a real-time logic for specifying properties of event-recording automata in a suitable way and demonstrate that the model checking problem for this logic is decidable.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy