Please use this identifier to cite or link to this item:
|Title:||Faster verification of RTL-specified systems via decomposition and constraint extension|
|Authors:||Andrei, Ş. |
|Source:||Andrei, Ş., Cheng, A.M.K. (2006). Faster verification of RTL-specified systems via decomposition and constraint extension. Proceedings - Real-Time Systems Symposium : 67-76. ScholarBank@NUS Repository. https://doi.org/10.1109/RTSS.2006.23|
|Abstract:||Embedded and real-time systems are increasingly common and complex, requiring formal specification and verification in order to guarantee their satisfaction of desirable safety and timing requirements. Real-Time Logic (RTL) has been used to capture both the specification of a real-time system and the desirable safety assertions with respect to this system specification. A verification procedure then determines whether the safety assertions hold with respect to the system specification. However, the satisfiability problem for RTL, as well as for other first-order logics, is undecidable. Consequently, efforts have been focused on identifying non-trivial classes of formulas sufficiently practical for describing industrial real-time systems for which the verification and debugging can be done via efficient heuristics. One such class of formulas is the so-called path RTL. The first contribution of this paper is to extend the existing path RTL class without sacrificing the time complexity of the traditional path RTL heuristic for verification. This implies that we can specify and verify real-time systems, which we were unable to do using the existing path RTL, in the extended path RTL. For real-time systems with large specifications, there is a lot of room for improvement in the algorithms used for verification and debugging. The second contribution of this paper is an efficient method to perform verification and debugging of real-time systems specifications using decomposition techniques. Our idea is to decompose the constraint graph, used in existing approaches, into independent subgraphs so that it is no longer necessary to analyze the entire specification at once, but rather its individual and smaller components. We have implemented this method in the Java-based DEVA-RTL tool and tested it on several industrial real-time systems. © 2006 IEEE.|
|Source Title:||Proceedings - Real-Time Systems Symposium|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Mar 7, 2018
WEB OF SCIENCETM
checked on Jan 24, 2018
checked on Mar 11, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.