FM 2006

Topic:

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

Objective:

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.

Prerequisites:

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