Scaling BDD-based timed verification with simulation reduction
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...
Saved in:
Main Authors: | , , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2016
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4944 https://ink.library.smu.edu.sg/context/sis_research/article/5947/viewcontent/scaling_bdd.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5947 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59472020-02-27T03:23:46Z Scaling BDD-based timed verification with simulation reduction NGUYEN, Truong Khanh TAN, Tian Huat SUN, Jun LI, Jiaying LIU, Yang CHEN, Manman DONG, Jin Song 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. 2016-11-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4944 info:doi/10.1007/978-3-319-47846-3_23 https://ink.library.smu.edu.sg/context/sis_research/article/5947/viewcontent/scaling_bdd.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Programming Languages and Compilers Software Engineering |
spellingShingle |
Programming Languages and Compilers Software Engineering NGUYEN, Truong Khanh TAN, Tian Huat SUN, Jun LI, Jiaying LIU, Yang CHEN, Manman DONG, Jin Song Scaling BDD-based timed verification with simulation reduction |
description |
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. |
format |
text |
author |
NGUYEN, Truong Khanh TAN, Tian Huat SUN, Jun LI, Jiaying LIU, Yang CHEN, Manman DONG, Jin Song |
author_facet |
NGUYEN, Truong Khanh TAN, Tian Huat SUN, Jun LI, Jiaying LIU, Yang CHEN, Manman DONG, Jin Song |
author_sort |
NGUYEN, Truong Khanh |
title |
Scaling BDD-based timed verification with simulation reduction |
title_short |
Scaling BDD-based timed verification with simulation reduction |
title_full |
Scaling BDD-based timed verification with simulation reduction |
title_fullStr |
Scaling BDD-based timed verification with simulation reduction |
title_full_unstemmed |
Scaling BDD-based timed verification with simulation reduction |
title_sort |
scaling bdd-based timed verification with simulation reduction |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2016 |
url |
https://ink.library.smu.edu.sg/sis_research/4944 https://ink.library.smu.edu.sg/context/sis_research/article/5947/viewcontent/scaling_bdd.pdf |
_version_ |
1770575154365071360 |