RTAS 2005 START ConferenceManager    

Systematic Debugging of Real-Time Systems based on Incremental Satisfiability Counting

Stefan ANDREI, Wei-Ngan CHIN, Albert M.K. CHENG, and Mihai LUPU

Presented at IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2005), San Francisco, California, March 7 - 10, 2005


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 a systematic debugging. The confidence of our approach is high as we have effectively evaluated SDRTL on several existing industrial based applications.

START Conference Manager (V2.47.7)
Maintainer: hjkim@redwood.snu.ac.kr