More about HKUST
Debugging and Verifying RTL-Specified Real-Time Systems via Incremental Satisfiability Counting
Speaker: Dr. Albert M. K. CHENG Real-Time Systems Laboratory University of Houston Title: "Debugging and Verifying RTL-Specified Real-Time Systems via Incremental Satisfiability Counting" Date: Thursday, 5 July 2007 Time: 4:00pm - 5:00pm Venue: Room 5487 (via lift nos. 25/26), HKUST Abstract: 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. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula can help us determine the specific constraints which should be added or modified to derive the expected solutions. This talk describes this debugging and verification approach, and shows how it can be applied to large-scale embedded/real-time systems. We have implemented this approach in a toolset consisting of ADRTL and DEVA-RTL, and have effectively evaluated it with several existing industrial applications, including the NASA X-38 Crew Return Vehicle avionics. ******************* Biography: Albert M. K. Cheng received the B.A. with Highest Honors in Computer Science, graduating Phi Beta Kappa, the M.S.in Computer Science with a minor in Electrical Engineering, and the Ph.D. in Computer Science, all from The University of Texas at Austin, where he held a GTE Foundation Doctoral Fellowship. Dr. Cheng is currently a tenured Associate Professor in the Department of Computer Science at the University of Houston, where he is the founding Director of the Real-Time Systems Laboratory. He has served as a technical consultant for several organizations, including IBM, and was also a visiting faculty in the Departments of Computer Science at Rice University (2000) and at the City University of Hong Kong (1995). Dr. Cheng is the author/co-author of over 100 refereed publications in real-time/embedded systems and related areas, and has received numerous awards, including the U.S. National Science Foundation Research Initiation Award (now known as the NSF CAREER award). His recent paper titled "Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting'' in the July 2006 issue of the IEEE Transactions on Computers has been selected as its Featured Article. He has been invited to present seminars, tutorials, and panel positions at over 30 conferences, has given invited seminars/keynotes at over 30 universities and organizations. He is and has been on the technical program committees of over 100 conferences, symposia, workshops, and editorial boards (including the IEEE Transactions on Software Engineering, 1998-2003). Currently, he is on the TPC of RTSS, RTAS, RTCSA, ESO, EC, ICEIS, ICINCO, SE, SEA, AIA, CNIS, CCN, ISC, and PDCN, and is the Program Chair of the 10th International Conference on SOFTWARE ENGINEERING AND APPLICATIONS (SEA), November 2006, Dallas, Texas. He is a Senior Member of the IEEE. Dr. Cheng is the author of the new senior/graduate-level textbook entitled Real-Time Systems: Scheduling, Analysis, and Verification (John Wiley & Sons), 2nd printing with updates, 2005.