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.
|