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.