loading...
Systematic Debugging of Real-Time Systems based on Incremental Satisfiability Counting
San Francisco, CA March 07-March 10
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTAS.2005.5011th IEEE Real Time and Embedded Tech ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Stefan Andrei, National University of Singapore
Albert M. K. Cheng, University of Houston
Wei-Ngan Chin, National University of Singapore
Miahi Lupu, National University of Singapore
Real-time logic (RTL) 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. This paper provides a first step towards this challenge. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula helps to determine the timing constraints which should be added or modified to the system's specification. We have implemented a tool (called SDRTL) that is able to perform systematic debugging. The confidence of our approach is high as we have evaluated SDRTL on several existing industrial-based applications.
Citation:
Stefan Andrei, Albert M. K. Cheng, Wei-Ngan Chin, Miahi Lupu, "Systematic Debugging of Real-Time Systems based on Incremental Satisfiability Counting," rtas, pp.519-528, 11th IEEE Real Time and Embedded Technology and Applications Symposium (RTAS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.