COLLOQUIUM Department of Computer Science and Engineering University of South Carolina Verification and Debugging of Real-Time Systems Specifications Stefan Andrei Department of Computer Science National University of Singapore Date: January 13, 2006 Time: 1530-1630 Place: Swearingen 1A03 (Faculty Lounge) Abstract Theorem proving is a challenging task for the formal verification of systems. We propose a new technique based on counting SAT-based (#SAT). A SAT solver tests if a propositional formula F has at least one truth assignment, whereas a #SAT solver returns the number of truth assignments of F. 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 is a daunting challenge. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula provides an indication of how “far away” a specification is from satisfying its safety assertion. Furthermore, specifications and safety assertions are often modified in an incremental fashion, where problematic bugs are fixed one at a time. In this way, we deterministically choose 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. We have evaluated SDRTL on several existing industrial based applications. While other incremental SAT solvers exist, to the best of our knowledge we present for the first time the theoretical background for the incremental counting satisfiability problem. Moreover, our proposed incremental algorithm is optimal as no unnecessary nodes are created during each counting. We believe that counting SAT can also be efficiently applied to other sub-areas of real-time systems, like scheduling analysis and to adjacent areas like digital circuits testing. Stefan Andrei is a Fellow (Visiting Assistant Professor) of the Department of Computer Science of National University of Singapore. He received his B.Sc. and M.Sc. in Computer Science, in 1994 and 1995, respectively, from the Alexander Ioan Cuza University in Iasi, Romania. He obtained his Ph.D. in Computer Science from Hamburg University in 2000. He was a postdoctoral Research Fellow of the National University of Singapore under the Singapore-MIT Alliance (SMA) between July 2002 and June 2005. He was a program committee member of the 11th International Conference on Real-Time and Embedded Computing Systems and Applications (RTCSA'05). His current research interests are real-time systems and programming languages, in particular verification and debugging of timing constraints, scheduling analysis, and digital circuits testing. More details can be found at http://www.comp.nus.edu.sg/~andrei/.