FM 2006

August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006


Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006

Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T2 Analysis and Verification of Real-Time/Embedded Software and Systems
Albert M. K. Cheng
University of Houston, USA
August 21, 2006 Time: 2:00-5:30, 1/2hr break at 3:30
Location: ITB 201
Format: Half-day (afternoon), handouts (part 1,part 2) will also be provided in printed form.


Introduction to the the state-of-the-art technology and available tools for the analysis and verification of real-time and embedded systems.


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. For example, when the driver of a car applies the brake, the anti-lock braking controller analyzes the environment in which the controller is embedded (car speed, road surface, direction of travel) and activates the brake with the appropriate frequency within fractions of a second. Both the result (brake activation) and the time at which the result is produced are important in ensuring the safety of the car, its driver and passengers.

Recently, computer hardware and software are increasingly embedded in a majority of these real-time 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. Examples of these real-time systems include computerized versions of the braking controller and the vital-sign monitor, the new generation of airplane and spacecraft avionics, the planned Space Station control software, high-performance network and telephone switching systems, multimedia tools, virtual reality systems, robotic controllers, and many safety-critical industrial applications. These embedded systems must satisfy stringent timing and reliability constraints in addition to functional correctness requirements.

There are two ways ensure system safety and reliability. One way is to employ engineering (both software and hardware) techniques such as structured programming principles to minimize implementation errors and then utilize testing techniques to uncover errors in the implementation. The other way is to use formal analysis and verification techniques to ensure that the implemented system satisfy the required safety constraints under all conditions given a set of assumptions. In a real-time system, not only do we need to satisfy stringent timing requirements, but also be able to guard against an imperfect execution environment which may violate pre-runtime design assumptions.

The first approach can only increase the confidence level we have on the correctness of the system because testing cannot guarantee that the system is error-free. The second approach can guarantee that a verified system always satisfies the checked safety properties.However, state-of-the-art techniques are often difficult to understand and to apply to realistic systems. Furthermore, it is often difficult to determine how practical a proposed technique is from the large number of mathematical notations used.

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 and embedded systems. Then the tutorial evaluates and assesses the practicality of the available techniques and tools for building the next generation of real-time and embedded systems. Topics covered includes analysis and verification, techniques/tools based on schedulability analysis (rate-monotonic and others), model checking, Statechart/Statemate, Modechart/Real-Time Logic (RTL, SDRTL, ADRTL), timed automata, timed Petri nets, process algebra, real-time temporal logic, and semantic rule-based analysis (EQL, MRL, OPS5). Non-masking fault-tolerance such as self-stabilization of time-critical procedural and rule systems will also be described.


Some programming experience in high-level programming language such as C/C++.

Biography of Tutor:

Albert M. K. Chengreceived 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).

He is the author/co-author of over 80 refereed publications in IEEE Transactions on Software Engineering (TSE), IEEE Transactions on Knowledge and Data Engineering (TKDE), Real-Time Systems Symposium (RTSS), Real-Time and Embedded Technology and Applications Symposium (RTAS), International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), and other leading conferences. One of his recent work presents a timing analysis of the NASA X-38 Space Station Crew Return Vehicle Avionics, which contains a fault-tolerant distributed system.

Dr. Cheng has received numerous awards, including the National Science Foundation Research Initiation Award (now known as the NSF CAREER award). He has been invited to present seminars and tutorials at over 30 conferences, and has given invited seminars/keynotes at over 30 universities and organizations, including the University of Texas at Dallas (2005); the 1st Intl. Conf. on Informatics in Control, Automation and Robotics (ICINCO), Setubal, Portugal (2004); and ICEIS, Ecole Superieure de l' Ouest (ESEO), Angers, France (2003).

He is and has been on the technical program committees of over 90 conferences, symposia, workshops, and editorial boards. He was an Associate Editor of the IEEE Transactions on Software Engineering (1998-2003), a Guest Co-Editor of two IEEE TSE Special Issues on Software and Performance (Nov. and Dec. 2000), a Guest Editor of the Special Issue on IEEE RTAS 2005 Work-in-Progress - ACM SIGBED Review (April 2005), an Associate Editor of the International Journal of Embedded Systems, an Associate Editor of the International Journal of Computer and Information Science, the work-in-progress program chair of the 2005 and 2001 IEEE-CS Real-Time Technology and Applications Symposium, the work-in-progress session chair of the 2003 IEEE-CS Real-Time Systems Symposium, the invited special panel chair for the software engineering for multimedia session at the 1999 IEEE-CS International Conference on Multimedia Computing Systems (ICMCS), and an invited panel speaker for the panel ``Software Engineering for Embedded Software: How Useful Are the Newer Paradigms?'' at SCOPES 2005 (Dallas, USA). Currently, he is on the TPC of RTSS, RTAS, RTCSA, ESO, EC, ICEIS, ICINCO, SE, SEA, AIA, CNIS, CCN, ISC, and PDCN. Dr. Cheng is an Honorary Member of the Institute for Systems and Technologies of Information, Control and Communication (INSTICC). He is a Senior Member of the IEEE.

Dr. Cheng is the author of several book chapters on E-commerce/Enterprise Information Systems, and an article entitled ``Embedded Operating Systems'' in the upcoming Encyclopedia of Computer Science and Engineering (John Wiley & Sons). He is the author of the new senior/graduate-level textbook entitled Real-Time Systems: Scheduling, Analysis, and Verification (John Wiley & Sons 2002, 2nd printing with updates 2005).