ERA-PAT

Automatic compositional verification of timed systems. Specification and verification of real-time systems are important research topics with crucial applications; however, the so-called state space explosion problem often prevents model checking to be used in practice for large systems. In this work, we present a self-contained toolkit to analyze real-time systems specified using event-recording automata (ERAs), which supports system modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that our tool outperforms the state-of-the-art timed model checker.

References in zbMATH (referenced in 2 articles , 1 standard article )

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

  1. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  2. Lin, Shang-Wei; Liu, Yang; Sun, Jun; Dong, Jin Song; André, Étienne: Automatic compositional verification of timed systems (2012) ioport