1999 Syposium for Applied Computing (ACM SAC'99)
Tutorial
Analysis and Verification of Real-Time Software and Systems
Albert M. K. Cheng
University of Houston-University Park
1:30 - 4:30PM
Abstract
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.