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.
|
Description
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.