Efficient Verification of Timed Automata with BDD-like Data-Structures
Resource
International Journal on Software Tools for Technology Transfer 6 (1): 77-97
Journal
International Journal on Software Tools for Technology Transfer
Journal Volume
6
Journal Issue
1
Pages
77-97
Date Issued
2004-07
Author(s)
Abstract
We investigate the effect on efficiency of various design issues for BDD-like data structures of TA state space representation and manipulation. We find that the efficiency is highly sensitive to decision atom design and canonical form definition. We explore the two issues in detail and propose to use CRD (Clock-Restriction Diagram) for TA state space representation and present algorithms for manipulating CRD in the verification of TAs. We compare three canonical forms for zones, develop a procedure for quick zone-containment detection, and present algorithms for verification with backward reachability analysis. Three possible evaluation orderings are also considered and discussed. We implement our idea in our tool Red 4.2 and carry out experiments to compare with other tools and various strategies of Red in both forward and backward analysis. Finally, we discuss the possibility of future improvement. © 2004 Springer-Verlag.
SDGs
Type
journal article
File(s)![Thumbnail Image]()
Loading...
Name
03.pdf
Size
905.05 KB
Format
Adobe PDF
Checksum
(MD5):bdb1111c513a03ee51f32177a2f495a3