Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2016

Abstract

Digitization is a technique that has been widely used in real-time model checking. With the assumption of digital clocks, symbolic model checking techniques (like those based on BDDs) can be applied for real-time systems. The problem of model checking real-time systems based on digitization is that the number of tick transitions increases rapidly with the increment of clock upper bounds. In this paper, we propose to improve BDD-based verification for real-time systems using simulation reduction. We show that simulation reduction allows us to verify timed automata with large clock upper bounds and to converge faster to the fixpoint. The presented approach is applied to reachability and LTL verification for real-time systems. Finally, we compare our approach with existing tools such as Rabbit, Uppaal, and CTAV and show that our approach outperforms them and achieves a significant speedup.

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 2015 International Symposium on Software Testing and Analysis, Baltimore, USA, July 13-17

Volume

10009

First Page

363

Last Page

382

ISBN

9783319478456

Identifier

10.1007/978-3-319-47846-3_23

Publisher

Springer Link

City or Country

Japan

Additional URL

https://doi.org/10.1007/978-3-319-47846-3_23

Download

Share

COinS