Abstract
The paper presents a new tool for automated verification of Timed Automata as well as protocols written in the specification language Estelle. The current version offers an automatic translation from Estelle specifications to timed automata, and two complementary methods of reachability analysis. The first one is based on Bounded Model Checking (BMC), while the second one is an on-the-fly verification on an abstract model of the system.
Partly supported by the State Committee for Scientific Research under the grant No. 8T11C 01419.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of LNCS, pages 322–335. Springer-Verlag, 1990.
J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of Uppaal. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998.
D. Beyer. Rabbit: Verification of real-time systems. In Proc. of the Workshop on Real-Time Tools (RT-TOOLS’01), pages 13–21, 2001.
M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. IF: An intermediate representation for SDL and its applications. In Proc. of SDL Forum’99, pages 423–440, 1999.
A. Cimatti, E. M. Clarke, F. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An open-source tool for symbolic model checking. In Proc. of CAV’02, volume 2404 of LNCS, pages 359–364. Springer-Verlag, 2002.
A. Doroś, A. Janowska, and P. Janowski. From specification languages to Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), volume 161(1) of Informatik-Berichte, pages 117–128. Humboldt University, 2002.
H. Garavel, F. Lang, and R. Mateescu. An overview of CADP 2001. Technical Report RT-254, INRIA Rhône-Alpes, 655, avenue de l’Europe, 38330 Montbonnot-St-Martin, December 2001.
G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Eng., 23(5):279–295, 1997.
ISO 8807 — information processing systems-Open System Interconnection. LOTOS — a formal description technique based on the temporal ordering of observational behaviour, 1989.
ISO/IEC 9074(E), Estelle-a formal description technique based on an extended state-transition model. International Standards Organization, 1997.
ITU-T Recommendation Z.100(11/99): Languages for telecommunication applications — Specification and Description Language, 1999.
K. McMillan. The SMV system. Technical Report CMU-CS-92-131, Carnegie-Mellon University, February 1992.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Cha.: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC’01), pages 530–535, June 2001.
W. Penczek, B. Woźna, and A. Zbrzezny. SAT-based bounded model checking for the universal fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01-237 Warsaw, August 2002.
W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pages 265–288. Springer-Verlag, 2002.
P. Pettersson and K. G. Larsen. Uppaal2k. Bulletin of the European Association for Theoretical Computer Science, 70:40–44, February 2000.
A. Półrola, W. Penczek, and M. Szreter. Reachability analysis for Timed Automata based on partitioning. Technical report, ICS PAS, Ordona 21, 01-237 Warsaw, 2003. to appear.
R. Sebastiani. Integrating SAT solvers with math reasoners: Foundations and basic algorithms. Technical Report 0111-22, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy, November 2001.
B. Woźna, W. Penczek, and A. Zbrzezny. Checking reachability properties for Timed Automata via SAT. Technical Report 949, ICS PAS, Ordona 21, 01-237 Warsaw, October 2002.
B. Woźna, W. Penczek, and A. Zbrzezny. Reachability for timed systems based on SAT-solvers. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), volume 161(2) of Informatik-Berichte, pages 380–395. Humboldt University, 2002.
S. Yovine. KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1(1/2):123–133, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dembiński, P. et al. (2003). √erics: A Tool for Verifying Timed Automata and Estelle Specifications. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_20
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive