1999 Syposium for Applied Computing (ACM SAC'99)


Analysis and Verification of Real-Time Software and Systems
Albert M. K. Cheng University of Houston-University Park

1:30 - 4:30PM


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. Recently, computer hardware and software are increasingly embedded in a majority of computer systems to monitor and control their operations. These computer systems are called embedded systems, real-time computer systems, or simply real-time systems. Unlike conventional, non-real-time computer systems, real-time computer systems are closely coupled with the environment being monitored and controlled. These embedded systems must satisfy stringent timing and reliability constraints in addition to functional correctness requirements. There are two ways to ensure that the implemented system satisfies the required safety and reliability constraints: employ engineering (both software and hardware) techniques such as structured programming principles and testing techniques or formal analysis and verification techniques. The objective of this tutorial is to provide an introduction to formal techniques and tools that are practical for actual use. These theoretical foundations are followed by practical examples that employ these advanced techniques to build, analyze, and verify different modules of real-time systems. The tutorial evaluates and assesses the practicality of the available techniques and tools for building the next generation of real-time systems. Topics covered include: formal verification techniques, schedulability analysis, model checking, Statechart/Statemate, Modechart, real-time temporal logic, and semantic rule-based analysis.

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 in 1990, 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. His research interests include real-time systems, rule-based expert systems, reliable software systems, multimedia tools, and fault-tolerant distributed and parallel systems. He is the author/co-author of over fifty refereed publications. He is a member of the honor societies of Phi Beta Kappa, Phi Kappa Phi, Upsilon Pi Epsilon, Beta Alpha Phi, and Golden Key. Dr. Cheng is an Associate Editor of the IEEE Transactions on Software Engineering, and a Senior Member of the IEEE.