 Shopping Bag ( 0 items )

All (11) from $63.60

New (4) from $111.45

Used (7) from $63.60
More About This Textbook
Overview
Editorial Reviews
From The Critics
This textbook introduces several approaches to the formal analysis and verification of realtime systems. Cheng (University of Houston) describes model checking of finite state system, visual formalism with statecharts, realtime logic, the Modechart specification, verification using time automata, and timed Petri nets. The final three chapters deal with rulebased expert systems. Annotation c. Book News, Inc., Portland, ORFrom the Publisher
"The author provides a substantial, uptodate overview of the verification and validation processâ€¦" (Computer Magazine, November 2004)"The unifying discussion on the formal analysis and verification methods are especially valuable and enlightening, both for graduate students and researchers." (International Journal of General Systems, December 2003)
Product Details
Related Subjects
Meet the Author
Read an Excerpt
RealTime Systems
Scheduling, Analysis, and VerificationBy Albert M. K. Cheng
John Wiley & Sons
ISBN: 0471184063Chapter One
INTRODUCTIONThe 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 realtime systems range from the antilock braking controller in automobiles to the vitalsign monitor in hospital intensivecare units. For example, when the driver of a car applies the brake, the antilock 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 realtime systems to monitor and control their operations. These computer systems are called embedded systems, realtime computer systems, or simply realtime systems. Unlike conventional, nonrealtime computer systems, realtime computer systems are closely coupled with the environment being monitored and controlled. Examples of realtime systems include computerized versions of the braking controller and the vitalsign monitor, the new generation of airplane and spacecraft avionics, the planned Space Station control software, highperformance network and telephone switching systems, multimedia tools, virtual reality systems, robotic controllers, batterypowered instruments, wireless communication devices (such as cellular phones and PDAs), astronomical telescopes with adaptiveoptics systems, and many safetycritical industrial applications. These embedded systems must satisfy stringent timing and reliability constraints in addition to functional correctness requirements.
Figure 1.1 shows a model of a realtime system. A realtime system has a decision component that interacts with the external environment (in which the decision component is embedded) by taking sensor readings and computing control decisions based on sensor readings and stored state information. We can characterize this realtime system model with seven components:
1. A sensor vector [bar.x] [member of] X,
2. A decision vector [bar.y] [member of] Y,
3. A system state vector [bar.s] [member of] S,
4. A set of environmental constraints A,
5. A decision map D, D : S x X [right arrow] S x Y,
6. A set of timing constraints T, and
7. A set of integrity constraints I.
In this model, X is the space of sensor input values, Y is the space of decision values, and S is the space of system state values. Let [bar.x](t) denote the value of the sensor input [bar.x] at time t, and so on.
The environmental constraints A are relations over X, Y, S and are assertions about the effect of a control decision on the external world which in turn affect future sensor input values. Environmental constraints are usually imposed by the physical environment in which the realtime decision system functions.
The decision map D relates [bar.y](t + 1), [bar.s](t + 1) to [bar.x](t), [bar.s](t), that is, given the current system state and sensor input, D determines the next decisions and system state values. Decision maps can be implemented by computer hardware and software components. A decision system need not be centralized, and may consist of a network of coordinating, distributed monitoring/decisionmaking components.
The decisions specified by D must conform to a set of integrity (safety) constraints I. Integrity constraints are relations over X, S, Y and are assertions that the decision map D must satisfy to ensure safe operation of the physical system under control. The implementation of the decision map D is subject to a set of timing constraints T, which are assertions about how fast the map D has to be performed. In addition, timing constraints exist on the environment (external to the decision system) that must be satisfied for the correct functioning of this environment.
There are two ways to 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 realtime system, we need to not only satisfy stringent timing requirements but also guard against an imperfect execution environment, which may violate preruntime 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 errorfree [Dahl, Dijkstra, and Hoare, 1972]. The second approach can guarantee that a verified system always satisfies the checked safety properties, and is the focus of this text.
However, stateoftheart techniques, which have been demonstrated in pedagogic systems, 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 book is to provide a more readable introduction to formal techniques that are practical for actual use. These theoretical foundations are followed by practical exercises in employing these advanced techniques to build, analyze, and verify different modules of realtime systems. Available specification analysis and verification tools are also described to help design and analyze realtime systems.
1.1 WHAT IS TIME?
Time is an essential concept in realtime systems, and keeping time using accurate clocks is thus required to ensure the correct operations of these systems. The master source for time is Paris's International Atomic Time (TAI), an average of several laboratory atomic clocks in the world. Since the earth's rotational rate slows by a few milliseconds each day, another master time source called the Universal Coordinated Time (UTC) performs leap corrections to the time provided by TAI while maintaining TAI's accuracy, making the time length of every natural solar day constant [Allan, Ashby, and Hodge, 1998].
UTC is used as the world time, and UTC time signals are sent from the National Institute of Standards and Technology (NIST) radio station, WWVB, in Fort Collins, Colorado, and other UTC radio stations to specialized receivers. Selected radios, receiverclocks, some phoneanswering systems, and even some VCRs have the capability to receive these UTC signals to maintain accurate clocks. Some computers have receivers to receive these UTC signals and thus the time provided by their internal clocks is as accurate as UTC. Note that depending on the location of the receiverclock, there is a delay in receiving the UTC signal. For instance, it takes around 5 ms for WWVB's UTC signal to get from Fort Collins to a receiverclock in my RealTime Systems Laboratory in Houston, Texas.
For computers whose time is kept by quartzbased computer clocks, we must ensure that these clocks are periodically synchronized such that they maintain a bounded drift relative to UTC. Software or logical clocks can be derived from computer clocks [Lamport, 1978]. In this text, when we refer to wall clock or absolute time, we refer to the standard time provided by a boundeddrift computer clock or UTC. Thus there is a mapping Clock: real time [right arrow] standard clock time.
1.2 SIMULATION
Simulation consists of constructing a model of an existing system to be studied or a system to be built and then executing actions allowed in this model. The model can be a physical entity like a scale clay model of an airplane or a computer representation. A computer model is often less costly than a physical model and can represent a noncomputer entity such as an airplane or its components as well as a computer entity such as a computer system or a program. A computer model also can represent a system with both computer and noncomputer components like an automobile with embedded computer systems to control its transmission and brakes.
This physical or computer model is called the simulator of the actual system. A simulator can carry out simulated executions of the simulated system and display the outcomes of these executions. A physical model of an airplane in a wind tunnel shows the aerodynamics of the simulated plane that is close to the actual plane. A software simulator on a singleprocessor system shows the performance of a network of personal computer workstations under a heavy network traffic condition. A software simulator can also be designed to simulate the behavior of an automobile crashing into a concrete barrier, showing its effects on the automobile's simulated occupants. Sometimes a simulator refers to a tool that can be programmed or directed without programming to mimic the events and actions in different systems. This simulator can be either computerbased (software, hardware, or both) or noncomputerbased.
Simulation is an inexpensive way to study the behavior of the simulated system and to study different ways to implement the actual system. If we detect behavior or events that are inconsistent with the specification and safety assertions, we can revise the model and thus the actual system to be built. In the case in which we consider several models as possible ways to implement the actual system, we can select the model that best satisfies the specification and safety assertions through the simulation and then implement it as the actual system.
Different levels of details of the actual system, also called the target system, can be modeled and its events simulated by a simulator. This makes it possible to study and observe only the relevant parts of the target system. For example, when designing and simulating the cockpit of an aircraft, we can restrict attention to that particular component by simulating only the cockpit with inputs and outputs to the other aircraft components, without simulating the behavior of the entire aircraft. In the design and simulation of a realtime multimedia communication system, we can simulate the traffic pattern between workstations but need not simulate the lowlevel signal processing involved in the coding and transmission processes if the performance is not affected by these lowlevel processes. The ability to simulate a target system at different detail levels or only a subset of its components reduces the resources needed for the simulation and decreases the complexity of the analysis of the simulation.
There are several simulation techniques in use, such as realtimeevent simulation and discreteevent simulation. A realtimeevent simulator like a physical scale model of an automobile performs its actions in realtime and the observable events are recorded in realtime. An example is the crash testing of the physical model of an automobile. Such a simulator requires recording instruments capable of recording events in realtime. When the physical model is actually an implemented target system, this is no longer a simulation but rather a testing of the actual system, as discussed below.
A discreteevent simulator, on the other hand, uses a logical clock(s) and is usually softwarebased. The variety of systems that can be represented by such a simulator is not limited by the speed at which the hardware executes the simulator since the simulated actions and events do not occur in realtime. Rather, they take place according to the speed of the simulator hardware and the instructions in the simulator program. Examples include the simulation of a network of computers in a singleprocessor system or the simulation of a faster microprocessor in a slower processor as in the design of popular nextgeneration personal computer microprocessors. Here, the appropriate actions and events "occur" at a particular logical time (representing realtime in the target system) depending on previous and current simulated actions and events. Entire books have been written that are devoted to discreteevent simulation.
Variations of simulation include the hybrid simulation approach, in which the simulator works with a partial implementation of the target system by acting as the nonimplemented part. As in the case of using only a simulator, the simulator here makes it possible to predict the performance and behavior of the target system once it is completely implemented.
One main disadvantage of simulation as a technique to analyze and verify realtime systems and other systems is that it is not able to model all possible eventaction sequences in the target system where the domain of possible sequences of observable events is infinite. Even when this domain is finite, the number of possible events is so large that the most powerful computer resources or physical instruments may not be able to trace through all possible sequences of events in the simulated target system.
1.3 TESTING
Testing is perhaps the oldest technique for detecting errors or problems in implemented software, hardware, or noncomputer systems. It consists of executing or operating (in the case of a noncomputer system) the system to be tested using a finite set of inputs and then checking to see if the corresponding outputs or behavior are correct with respect to the specifications. To test a realtime system, the values as well as the timing of the inputs are important. Similarly, both the output values and the time at which they are produced must be checked for correctness.
Many approaches have been developed for testing software, hardware, and noncomputer systems. The simplest technique is of course to perform an exhaustive test run of the system with every possible input and then to check if the corresponding output is correct. This approach is not practical except for small systems with limited input space. For larger systems, the time needed to test is prohibitively long. For systems with an infinite number of possible inputs, this approach is of course not viable. Since relatively little training is required on the part of the testing personnel, testing has been and will continue to be used extensively in industry.
There are three common techniques for software testing in the current stateofthepractice: functional testing, structural testing, and code reading.
Continues...
Table of Contents
LIST OF FIGURES.
1 INTRODUCTION.
1.1 What Is Time?
1.2 Simulation.
1.3 Testing.
1.4 Verification.
1.5 RunTime Monitoring.
1.6 Useful Resources.
2 ANALYSIS AND VERIFICATION OF NONREALTIME SYSTEMS.
2.1 Symbolic Logic.
2.2 Automata and Languages.
2.3 Historical Perspective and Related Work.
2.4 Summary.
Exercises.
3 REALTIME SCHEDULING AND SCHEDULABILITY ANALYSIS.
3.1 Determining Computation Time.
3.2 Uniprocessor Scheduling.
3.3 Multiprocessor Scheduling.
3.4 Available Scheduling Tools.
3.5 Available RealTime Operating Systems.
3.6 Historical Perspective and Related Work.
3.7 Summary.
Exercises.
4 MODEL CHECKING OF FINITESTATE SYSTEMS.
4.1 System Specification.
4.2 ClarkeEmersonSistla Model Checker.
4.3 Extensions to CTL.
4.4 Applications.
4.5 Complete CTL Model Checker in C.
4.6 Symbolic Model Checking.
4.7 RealTime CTL.
4.8 Available Tools.
4.9 Historical Perspective and Related Work.
4.10 Summary.
Exercises.
5 VISUAL FORMALISM, STATECHARTS, AND STATEMATE.
5.1 Statecharts.
5.2 ActivityCharts.
5.3 ModuleCharts.
5.4 STATEMATE.
5.5 Available Tools.
5.6 Historical Perspective and Related Work.
5.7 Summary.
Exercises.
6 REALTIME LOGIC, GRAPHTHEORETIC ANALYSIS, AND MODECHART.
6.1 Specification and Safety Assertions.
6.2 EventAction Model.
6.3 RealTime Logic.
6.4 Restricted RTL Formulas.
6.5 Checking for Unsatisfiability.
6.6 Efficient Unsatisfiability Check.
6.7 Industrial Example: NASA X38 Crew Return Vehicle.
6.8 Modechart Specification Language.
6.9 Verifying Timing Properties of Modechart Specifications.
6.10 Available Tools.
6.11 Historical Perspective and Related Work.
6.12 Summary.
Exercises.
7 VERIFICATION USING TIMED AUTOMATA.
7.1 LynchVaandrager AutomataTheoretic Approach.
7.2 AlurDill AutomataTheoretic Approach.
7.3 AlurDill Region Automaton and Verification.
7.4 Available Tools.
7.5 Historical Perspective and Related Work.
7.6 Summary.
Exercises.
8 TIMED PETRI NETS.
8.1 Untimed Petri Nets.
8.2 Petri Nets with Time Extensions.
8.3 Time ER Nets.
8.4 Properties of HighLevel Petri Nets.
8.5 BerthomieuDiaz Analysis Algorithm for TPNs.
8.6 Milano Group's Approach to HLTPN Analysis.
8.7 Practicality: Available Tools.
8.8 Historical Perspective and Related Work.
8.9 Summary.
Exercises.
9 PROCESS ALGEBRA.
9.1 Untimed Process Algebras.
9.2 Milner's Calculus of Communicating Systems.
9.3 Timed Process Algebras.
9.4 Algebra of Communicating Shared Resources.
9.5 Analysis and Verification.
9.6 Relationships to Other Approaches.
9.7 Available Tools.
9.8 Historical Perspective and Related Work.
9.9 Summary.
Exercises.
10 DESIGN AND ANALYSIS OF PROPOSITIONALLOGIC RULEBASED SYSTEMS.
10.1 RealTime Decision Systems.
10.2 RealTime Expert Systems.
10.3 PropositionalLogic RuleBased Programs: the EQL Language.
10.4 StateSpace Representation.
10.5 ComputerAided Design Tools.
10.6 The Analysis Problem.
10.7 Industrial Example: Analysis of the Cryogenic Hydrogen Pressure Malfunction Procedure of the Space Shuttle Vehicle Pressure Control System.
10.8 The Synthesis Problem.
10.9 Specifying Termination Conditions in Estella.
10.10 Two Industrial Examples.
10.11 The EstellaGeneral Analysis Tool.
10.12 Quantitative Timing Analysis Algorithms.
10.13 Historical Perspective and Related Work.
10.14 Summary.
Exercises.
11 TIMING ANALYSIS OF PREDICATELOGIC RULEBASED SYSTEMS.
11.1 The OPS5 Language.
11.2 ChengTsai Timing Analysis Methodology.
11.3 ChengChen Timing Analysis Methodology.
11.4 Historical Perspective and Related Work.
11.5 Summary.
Exercises.
12 OPTIMIZATION OF RULEBASED SYSTEMS.
12.1 Introduction.
12.2 Background.
12.3 Basic Definitions.
12.4 Optimization Algorithm.
12.5 Experimental Evaluation.
12.6 Comments on Optimization Methods.
12.7 Historical Perspective and Related Work.
12.8 Summary.
Exercises.
BIBLIOGRAPHY.
INDEX.