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