Verics

√erics: A Tool for Verifying Timed Automata and Estelle Specifications. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  2. Belardinelli, F.; Lomuscio, A.: Quantified epistemic logics for reasoning about knowledge in multi-agent systems (2009)
  3. Dembiński, Piotr; Janowska, Agata; Janowski, Paweł; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Wozna, Bozena; Zbrzezny, Andrzej: $\surd$erics: A tool for verifying timed automata and Estelle specifications (2003)