Please use this identifier to cite or link to this item:
Title: Automatic debugging of real-time systems based on incremental satisfiability counting
Authors: Andrei, Ş. 
Chin, W.N. 
Cheng, A.M.K.
Lupu, M.
Keywords: Automatic debugging
Counting SAT problem
Formal methods
Incremental computation
Real-time system
System development tools
Timing constraint
Issue Date: 2006
Citation: Andrei, Ş., Chin, W.N., Cheng, A.M.K., Lupu, M. (2006). Automatic debugging of real-time systems based on incremental satisfiability counting. IEEE Transactions on Computers 55 (7) : 830-842. ScholarBank@NUS Repository.
Abstract: Real-time logic (RTL) [2], [3], [4] is useful for the verification of a safety assertion with respect to the specification of a real-time system. Since the satisfiability problem for RTL is undecidable, the systematic debugging of a real-time system appears impossible. A first step toward this challenge was presented in [1]. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula can help us determine the specific constraints which should be added or modified to get the expected solutions. This paper solves an even more challenging problem specified as future work in [1], namely, the embedding and the integration of our debugger in autonomous systems which generate real-time control plans on-the-fly, since these specifications must meet timing constraints, but without human interaction. The idea is to consider in advance all the necessary information, such as the designer's guidance. We have implemented a tool (called ADRTL) that is able to perform automatic debugging. The confidence of our approach is high as we have successfully evaluated ADRTL on several existing industrial-based applications. © 2006 IEEE.
Source Title: IEEE Transactions on Computers
ISSN: 00189340
DOI: 10.1109/TC.2006.97
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Apr 4, 2020


checked on Mar 18, 2020

Page view(s)

checked on Mar 31, 2020

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.