Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

8-2012

Abstract

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.

Keywords

Model Check, Proof Rule, Monolithic Approach, State Space Explosion Problem, UPPAAL Model

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 18th International Symposium Paris, France, 2012 August 27-31

First Page

272

Last Page

276

ISBN

9783642327582

Identifier

10.1007/978-3-642-32759-9_24

Publisher

Springer Link

City or Country

Paris, France

Additional URL

https://doi.org/10.1007/978-3-642-32759-9_24

Share

COinS