Systematic/Automatic Debugging for path Real Time Logic -- SDRTL/ADRTL


People Papers Tool description Java docs



Keywords: system development tools, systematic debugging, formal methods, timing constraint, #SAT problem, incremental computation




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 looks 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 can help us determine possible differences from the expected solutions. We have implemented a tool (SDRTL) that is able to perform a systematic debugging. The confidence of our approach is high since we have effectively evaluated SDRTL on several industrial real applications.