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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., … Zbrzezny, A. (2003). √erics: A tool for verifying timed automata and Estelle specifications. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2619, 278–283. https://doi.org/10.1007/3-540-36577-x_20
Mendeley helps you to discover research relevant for your work.