Dr. Albert M. K. Cheng - University of Houston
Students: Spring 2024, unless noted otherwise, sessions will be virtual on Zoom.
Automatic Debugging and Verification of RTL-Specified Real-Time Systems via Incremental Satisfiability Counting and On-Time and Scalable Intrusion Detection in Embedded Systems
Mar 28, 2007
Download:
MP4 Video Size: 220.1MB
Watch on YouTube
Abstract
Abstract 1: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 approach and how it can be embedded into autonomous systems. We have implemented a tool called ADRTL for automatic debugging of RTL specifications. The confidence of our approach is high as we have effectively evaluated ADRTL on several existing industrial applications, including the NASA X-38 Crew Return Vehicle avionics.
Abstract 2:
Embedded systems are becoming ubiquitous and are increasingly interconnected or networked, making them more vulnerable to security attacks. A large class of these systems such as SCADA and PCS has real-time and safety constraints. Therefore, in addition to satisfying these requirements, achieving system security emerges as a critical challenge to ensure that users can trust these embedded systems to perform correct operations. One objective in a secure system is to identify attacks by detecting anomalous system behaviors. This part of the talk describes the challenges in the design and implementation of such intrusion detection system (IDS), addressing (1) accuracy: the IDS identifies no or as few false positives as the resource (time, space, power, etc.) and/or policy constraints allow, and no or as few false negatives as the resource and/or policy constraints allow; (2) efficiency/timeliness: the IDS does not violate the host embedded system's application deadlines and has a reasonable space overhead; (3) scalability: the IDS can scale to work with large embedded systems; and (4) power-awareness: the IDS does not significantly reduce the operational period of battery-powered embedded systems. We conclude with an outline of one of several promising embedded IDS approaches under investigation. This approach is based on automatic rule-base generation and semantic analysis.
About the Speaker
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.
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.
Ways to Watch
