| Title: | Verification and debugging of real-time systems using counting SAT |
| Date: |
August 19, 2005 (Friday)
|
| Time: |
2:30 p.m. - 3:30 p.m.
|
| Venue: |
Room 121, 1/F, Ho Sin-hang Engineering Building,
The Chinese University of Hong Kong, Shatin, N.T. |
| Speaker: |
Dr Stefan Andrei
Department of Computer Science National University of Singapore Singapore |
Theorem proving is a challenging task for formal verification of systems. There exist many efforts to efficiently solve this problem, based for example on rewriting rules and/or SAT-based techniques. We propose an alternative of SAT-based techniques by using instead a counting SAT-based technique (denoted also as #SAT). A SAT solver tests if a propositional formula F has at least one truth assignment, while 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 appears impossible. This work 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 decides how "far away" is a given specification 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. The confidence of our approach is high as we have effectively evaluated SDRTL on several existing industrial based applications.
While there exist incremental SAT solvers, to the best of our knowledge, our earlier contribution presents 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 believed 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.
BIOGRAPHY:
Stefan Andrei is a Fellow of the National University of Singapore, School of Computing. He has received his B.Sc. and M.Sc. in Computer Science, in 1994 and 1995, respectively, from "Al.I.Cuza" University of lasi, Romania and Ph.D. in Computer Science in 2000 from the Hamburg University, Germany. Between 1997 and 2000, he got the following academic awards: DAAD scholarship (German Government), TEMPUS S_JEP 11168-96 fellowship (European Union) and World Bank Joint Japan Graduate Scholarship (United States) at Fachbereich Informatik, Hamburg Universitaet, Germany. He is a member of the Editorial Board of Scientific Annals of "Al.I.Cuza" University of Iasi. He was a Program Committee member and a Chairman of Romanian Symposium on Computer Science (ROSYCS'04 - Web Technologies). He is 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, in particular verification and debugging of timing constraints, scheduling analysis, digital circuits testing, and so on. More details about him can be found at http://www.comp.nus.edu.sg/~andrei/
Enquiries: Miss Temmy So at tel 2609 8444
For more information, please refer to http://www.cse.cuhk.edu.hk/seminar