SAC 2000 Tutorial

Analysis and Verification of Real-Time Software and Systems

Albert M. K. Cheng, Rice University and University of Houston-University Park
Audience: Anyone interested in the state-of-the-art technology and available tools for formal analysis and verification of real-time systems for monitoring, communication, control, and decision making.
Audience Background: Some programming experience.
Duration: 3 hours.


The correctness of many systems and devices in our modern society depends not only on the effects or results they produce, but also on the time at which these results are produced. These real-time systems range from the anti-lock braking controller in automobiles to the vital-sign monitor in hospital intensive-care units. Recently, computer hardware and software are increasingly embedded in a majority of these real-time systems to monitor and control their operations. These embedded systems must satisfy stringent timing and reliability constraints in addition to functional correctness requirements. The objective of this tutorial is to provide a introduction to formal techniques and tools that are practical for actual use. These theoretical foundations are followed by practical examples in employing these advanced techniques to build, analyze, and verify different modules of real-time systems. Then the tutorial evaluates and assesses the practicality of the available techniques and tools for building the next generation of real-time systems, such as the the X-38 Space Station Crew Return Vehicle Avionics (containing a fault-tolerant distributed system) which has been analyzed by the instructor for timing correctness. Topics covered include the analysis and verification techniques/tools based on schedulability analysis, model checking, Statechart/Statemate, Modechart, timed automata, timed Petri nets, process algebra, real-time temporal logic, and semantic rule-based analysis.

The material presented in this tutorial is based upon work supported in part by the National Science Foundation under Award Nos. CCR-9111563 and IRI-9526004, by the Texas Advanced Research Program under Grant No. 3652270, and by a grant from the University of Houston Institute of Space Systems Operations.

The Presenter

Dr. 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 also 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--University Park, where he is the founding Director of the Real-Time Systems Laboratory. He has served as a technical consultant for several organizations, including IBM. During the summer 1995, he was a visiting professor at the City University of Hong Kong. He has been invited by Rice University's Department of Computer Science in August 1999 to hold a visiting faculty position there.

His research interests include real-time systems, rule-based expert systems, reliable software systems, multimedia tools, and fault-tolerant distributed and parallel systems. One of his recent work presents a timing analysis of the X-38 Space Station Crew Return Vehicle Avionics, which contains a fault-tolerant distributed system. He is the author/co-author of over fifty refereed publications; he is serving and has served on the program committees of many conferences in his areas of research (including ICECCS, IC3N, CIKM, PDCS, COMPASS, ICTAI, CAIA, ICDE, and HICSS). He is a frequent reviewer for the IEEE-CS Publications Office as well as for many journals and conferences,

Dr. Cheng has received numerous awards, including the National Science Foundation Research Initiation Award, the Texas Higher Education Coordinating Board Advanced Research Program Award, and the University of Houston Research Initiation Grant. He has been nominated for the 1999 University of Houston Teaching Excellence Award by his students and colleagues for his outstanding teaching. He is a member of the honor societies of Phi Beta Kappa, Phi Kappa Phi, Upsilon Pi Epsilon, Beta Alpha Phi, and Golden Key. He has been invited to present seminars/keynotes and tutorials at over 25 conferences, and has given invited seminars at many universities and organizations. He is the invited Session/Panel Chair of the Special Session on Software Engineering for Multimedia, IEEE Intl. Conf. on Multimedia Computer Systems (ICMCS), Florence, Italy, June 1999. He is an Associate Editor of the IEEE Transactions on Software Engineering, a Guest Co-Editor of an upcoming IEEE TSE Special Issue on Software and Performance (2000), and the Guest Editor of a Special Issue on Real-Time AI Systems of the IEEE Intelligent Systems (2000). Dr. Cheng is a Senior Member of the IEEE.