AMK Cheng
John Wiley & Sons
e druk, 2002
9780471184065
Real–Time Systems – Scheduling, Analysis and Verification
Scheduling, Analysis, and Verification
Specificaties
Gebonden, 552 blz.
|
Engels
John Wiley & Sons |
e druk, 2002
ISBN13: 9780471184065
Rubricering
Verwachte levertijd ongeveer 9 werkdagen
Samenvatting
The first book to provide a comprehensive overview of the subject rather than a collection of papers.
The author is a recognized authority in the field as well as an outstanding teacher lauded for his ability to convey these concepts clearly to many different audiences.
A handy reference for practitioners in the field.
Specificaties
Inhoudsopgave
PREFACE.
<br />
<br /> LIST OF FIGURES.
<br />
<br /> 1 INTRODUCTION.
<br />
<br /> 1.1 What Is Time?
<br />
<br /> 1.2 Simulation.
<br />
<br /> 1.3 Testing.
<br />
<br /> 1.4 Verification.
<br />
<br /> 1.5 Run–Time Monitoring.
<br />
<br /> 1.6 Useful Resources.
<br />
<br /> 2 ANALYSIS AND VERIFICATION OF NON–REAL–TIME SYSTEMS.
<br />
<br /> 2.1 Symbolic Logic.
<br />
<br /> 2.2 Automata and Languages.
<br />
<br /> 2.3 Historical Perspective and Related Work.
<br />
<br /> 2.4 Summary.
<br />
<br /> Exercises.
<br />
<br /> 3 REAL–TIME SCHEDULING AND SCHEDULABILITY ANALYSIS.
<br />
<br /> 3.1 Determining Computation Time.
<br />
<br /> 3.2 Uniprocessor Scheduling.
<br />
<br /> 3.3 Multiprocessor Scheduling.
<br />
<br /> 3.4 Available Scheduling Tools.
<br />
<br /> 3.5 Available Real–Time Operating Systems.
<br />
<br /> 3.6 Historical Perspective and Related Work.
<br />
<br /> 3.7 Summary.
<br />
<br /> Exercises.
<br />
<br /> 4 MODEL CHECKING OF FINITE–STATE SYSTEMS.
<br />
<br /> 4.1 System Specification.
<br />
<br /> 4.2 Clarke–Emerson–Sistla Model Checker.
<br />
<br /> 4.3 Extensions to CTL.
<br />
<br /> 4.4 Applications.
<br />
<br /> 4.5 Complete CTL Model Checker in C.
<br />
<br /> 4.6 Symbolic Model Checking.
<br />
<br /> 4.7 Real–Time CTL.
<br />
<br /> 4.8 Available Tools.
<br />
<br /> 4.9 Historical Perspective and Related Work.
<br />
<br /> 4.10 Summary.
<br />
<br /> Exercises.
<br />
<br /> 5 VISUAL FORMALISM, STATECHARTS, AND STATEMATE.
<br />
<br /> 5.1 Statecharts.
<br />
<br /> 5.2 Activity–Charts.
<br />
<br /> 5.3 Module–Charts.
<br />
<br /> 5.4 STATEMATE.
<br />
<br /> 5.5 Available Tools.
<br />
<br /> 5.6 Historical Perspective and Related Work.
<br />
<br /> 5.7 Summary.
<br />
<br /> Exercises.
<br />
<br /> 6 REAL–TIME LOGIC, GRAPH–THEORETIC ANALYSIS, AND MODECHART.
<br />
<br /> 6.1 Specification and Safety Assertions.
<br />
<br /> 6.2 Event–Action Model.
<br />
<br /> 6.3 Real–Time Logic.
<br />
<br /> 6.4 Restricted RTL Formulas.
<br />
<br /> 6.5 Checking for Unsatisfiability.
<br />
<br /> 6.6 Efficient Unsatisfiability Check.
<br />
<br /> 6.7 Industrial Example: NASA X–38 Crew Return Vehicle.
<br />
<br /> 6.8 Modechart Specification Language.
<br />
<br /> 6.9 Verifying Timing Properties of Modechart Specifications.
<br />
<br /> 6.10 Available Tools.
<br />
<br /> 6.11 Historical Perspective and Related Work.
<br />
<br /> 6.12 Summary.
<br />
<br /> Exercises.
<br />
<br /> 7 VERIFICATION USING TIMED AUTOMATA.
<br />
<br /> 7.1 Lynch–Vaandrager Automata–Theoretic Approach.
<br />
<br /> 7.2 Alur–Dill Automata–Theoretic Approach.
<br />
<br /> 7.3 Alur–Dill Region Automaton and Verification.
<br />
<br /> 7.4 Available Tools.
<br />
<br /> 7.5 Historical Perspective and Related Work.
<br />
<br /> 7.6 Summary.
<br />
<br /> Exercises.
<br />
<br /> 8 TIMED PETRI NETS.
<br />
<br /> 8.1 Untimed Petri Nets.
<br />
<br /> 8.2 Petri Nets with Time Extensions.
<br />
<br /> 8.3 Time ER Nets.
<br />
<br /> 8.4 Properties of High–Level Petri Nets.
<br />
<br /> 8.5 Berthomieu–Diaz Analysis Algorithm for TPNs.
<br />
<br /> 8.6 Milano Group′s Approach to HLTPN Analysis.
<br />
<br /> 8.7 Practicality: Available Tools.
<br />
<br /> 8.8 Historical Perspective and Related Work.
<br />
<br /> 8.9 Summary.
<br />
<br /> Exercises.
<br />
<br /> 9 PROCESS ALGEBRA.
<br />
<br /> 9.1 Untimed Process Algebras.
<br />
<br /> 9.2 Milner′s Calculus of Communicating Systems.
<br />
<br /> 9.3 Timed Process Algebras.
<br />
<br /> 9.4 Algebra of Communicating Shared Resources.
<br />
<br /> 9.5 Analysis and Verification.
<br />
<br /> 9.6 Relationships to Other Approaches.
<br />
<br /> 9.7 Available Tools.
<br />
<br /> 9.8 Historical Perspective and Related Work.
<br />
<br /> 9.9 Summary.
<br />
<br /> Exercises.
<br />
<br /> 10 DESIGN AND ANALYSIS OF PROPOSITIONAL–LOGIC RULE–BASED SYSTEMS.
<br />
<br /> 10.1 Real–Time Decision Systems.
<br />
<br /> 10.2 Real–Time Expert Systems.
<br />
<br /> 10.3 Propositional–Logic Rule–Based Programs: the EQL Language.
<br />
<br /> 10.4 State–Space Representation.
<br />
<br /> 10.5 Computer–Aided Design Tools.
<br />
<br /> 10.6 The Analysis Problem.
<br />
<br /> 10.7 Industrial Example: Analysis of the Cryogenic Hydrogen Pressure Malfunction Procedure of the Space Shuttle Vehicle Pressure Control System.
<br />
<br /> 10.8 The Synthesis Problem.
<br />
<br /> 10.9 Specifying Termination Conditions in Estella.
<br />
<br /> 10.10 Two Industrial Examples.
<br />
<br /> 10.11 The Estella–General Analysis Tool.
<br />
<br /> 10.12 Quantitative Timing Analysis Algorithms.
<br />
<br /> 10.13 Historical Perspective and Related Work.
<br />
<br /> 10.14 Summary.
<br />
<br /> Exercises.
<br />
<br /> 11 TIMING ANALYSIS OF PREDICATE–LOGIC RULE–BASED SYSTEMS.
<br />
<br /> 11.1 The OPS5 Language.
<br />
<br /> 11.2 Cheng–Tsai Timing Analysis Methodology.
<br />
<br /> 11.3 Cheng–Chen Timing Analysis Methodology.
<br />
<br /> 11.4 Historical Perspective and Related Work.
<br />
<br /> 11.5 Summary.
<br />
<br /> Exercises.
<br />
<br /> 12 OPTIMIZATION OF RULE–BASED SYSTEMS.
<br />
<br /> 12.1 Introduction.
<br />
<br /> 12.2 Background.
<br />
<br /> 12.3 Basic Definitions.
<br />
<br /> 12.4 Optimization Algorithm.
<br />
<br /> 12.5 Experimental Evaluation.
<br />
<br /> 12.6 Comments on Optimization Methods.
<br />
<br /> 12.7 Historical Perspective and Related Work.
<br />
<br /> 12.8 Summary.
<br />
<br /> Exercises.
<br />
<br /> BIBLIOGRAPHY.
<br />
<br /> INDEX.
<br />
<br /> LIST OF FIGURES.
<br />
<br /> 1 INTRODUCTION.
<br />
<br /> 1.1 What Is Time?
<br />
<br /> 1.2 Simulation.
<br />
<br /> 1.3 Testing.
<br />
<br /> 1.4 Verification.
<br />
<br /> 1.5 Run–Time Monitoring.
<br />
<br /> 1.6 Useful Resources.
<br />
<br /> 2 ANALYSIS AND VERIFICATION OF NON–REAL–TIME SYSTEMS.
<br />
<br /> 2.1 Symbolic Logic.
<br />
<br /> 2.2 Automata and Languages.
<br />
<br /> 2.3 Historical Perspective and Related Work.
<br />
<br /> 2.4 Summary.
<br />
<br /> Exercises.
<br />
<br /> 3 REAL–TIME SCHEDULING AND SCHEDULABILITY ANALYSIS.
<br />
<br /> 3.1 Determining Computation Time.
<br />
<br /> 3.2 Uniprocessor Scheduling.
<br />
<br /> 3.3 Multiprocessor Scheduling.
<br />
<br /> 3.4 Available Scheduling Tools.
<br />
<br /> 3.5 Available Real–Time Operating Systems.
<br />
<br /> 3.6 Historical Perspective and Related Work.
<br />
<br /> 3.7 Summary.
<br />
<br /> Exercises.
<br />
<br /> 4 MODEL CHECKING OF FINITE–STATE SYSTEMS.
<br />
<br /> 4.1 System Specification.
<br />
<br /> 4.2 Clarke–Emerson–Sistla Model Checker.
<br />
<br /> 4.3 Extensions to CTL.
<br />
<br /> 4.4 Applications.
<br />
<br /> 4.5 Complete CTL Model Checker in C.
<br />
<br /> 4.6 Symbolic Model Checking.
<br />
<br /> 4.7 Real–Time CTL.
<br />
<br /> 4.8 Available Tools.
<br />
<br /> 4.9 Historical Perspective and Related Work.
<br />
<br /> 4.10 Summary.
<br />
<br /> Exercises.
<br />
<br /> 5 VISUAL FORMALISM, STATECHARTS, AND STATEMATE.
<br />
<br /> 5.1 Statecharts.
<br />
<br /> 5.2 Activity–Charts.
<br />
<br /> 5.3 Module–Charts.
<br />
<br /> 5.4 STATEMATE.
<br />
<br /> 5.5 Available Tools.
<br />
<br /> 5.6 Historical Perspective and Related Work.
<br />
<br /> 5.7 Summary.
<br />
<br /> Exercises.
<br />
<br /> 6 REAL–TIME LOGIC, GRAPH–THEORETIC ANALYSIS, AND MODECHART.
<br />
<br /> 6.1 Specification and Safety Assertions.
<br />
<br /> 6.2 Event–Action Model.
<br />
<br /> 6.3 Real–Time Logic.
<br />
<br /> 6.4 Restricted RTL Formulas.
<br />
<br /> 6.5 Checking for Unsatisfiability.
<br />
<br /> 6.6 Efficient Unsatisfiability Check.
<br />
<br /> 6.7 Industrial Example: NASA X–38 Crew Return Vehicle.
<br />
<br /> 6.8 Modechart Specification Language.
<br />
<br /> 6.9 Verifying Timing Properties of Modechart Specifications.
<br />
<br /> 6.10 Available Tools.
<br />
<br /> 6.11 Historical Perspective and Related Work.
<br />
<br /> 6.12 Summary.
<br />
<br /> Exercises.
<br />
<br /> 7 VERIFICATION USING TIMED AUTOMATA.
<br />
<br /> 7.1 Lynch–Vaandrager Automata–Theoretic Approach.
<br />
<br /> 7.2 Alur–Dill Automata–Theoretic Approach.
<br />
<br /> 7.3 Alur–Dill Region Automaton and Verification.
<br />
<br /> 7.4 Available Tools.
<br />
<br /> 7.5 Historical Perspective and Related Work.
<br />
<br /> 7.6 Summary.
<br />
<br /> Exercises.
<br />
<br /> 8 TIMED PETRI NETS.
<br />
<br /> 8.1 Untimed Petri Nets.
<br />
<br /> 8.2 Petri Nets with Time Extensions.
<br />
<br /> 8.3 Time ER Nets.
<br />
<br /> 8.4 Properties of High–Level Petri Nets.
<br />
<br /> 8.5 Berthomieu–Diaz Analysis Algorithm for TPNs.
<br />
<br /> 8.6 Milano Group′s Approach to HLTPN Analysis.
<br />
<br /> 8.7 Practicality: Available Tools.
<br />
<br /> 8.8 Historical Perspective and Related Work.
<br />
<br /> 8.9 Summary.
<br />
<br /> Exercises.
<br />
<br /> 9 PROCESS ALGEBRA.
<br />
<br /> 9.1 Untimed Process Algebras.
<br />
<br /> 9.2 Milner′s Calculus of Communicating Systems.
<br />
<br /> 9.3 Timed Process Algebras.
<br />
<br /> 9.4 Algebra of Communicating Shared Resources.
<br />
<br /> 9.5 Analysis and Verification.
<br />
<br /> 9.6 Relationships to Other Approaches.
<br />
<br /> 9.7 Available Tools.
<br />
<br /> 9.8 Historical Perspective and Related Work.
<br />
<br /> 9.9 Summary.
<br />
<br /> Exercises.
<br />
<br /> 10 DESIGN AND ANALYSIS OF PROPOSITIONAL–LOGIC RULE–BASED SYSTEMS.
<br />
<br /> 10.1 Real–Time Decision Systems.
<br />
<br /> 10.2 Real–Time Expert Systems.
<br />
<br /> 10.3 Propositional–Logic Rule–Based Programs: the EQL Language.
<br />
<br /> 10.4 State–Space Representation.
<br />
<br /> 10.5 Computer–Aided Design Tools.
<br />
<br /> 10.6 The Analysis Problem.
<br />
<br /> 10.7 Industrial Example: Analysis of the Cryogenic Hydrogen Pressure Malfunction Procedure of the Space Shuttle Vehicle Pressure Control System.
<br />
<br /> 10.8 The Synthesis Problem.
<br />
<br /> 10.9 Specifying Termination Conditions in Estella.
<br />
<br /> 10.10 Two Industrial Examples.
<br />
<br /> 10.11 The Estella–General Analysis Tool.
<br />
<br /> 10.12 Quantitative Timing Analysis Algorithms.
<br />
<br /> 10.13 Historical Perspective and Related Work.
<br />
<br /> 10.14 Summary.
<br />
<br /> Exercises.
<br />
<br /> 11 TIMING ANALYSIS OF PREDICATE–LOGIC RULE–BASED SYSTEMS.
<br />
<br /> 11.1 The OPS5 Language.
<br />
<br /> 11.2 Cheng–Tsai Timing Analysis Methodology.
<br />
<br /> 11.3 Cheng–Chen Timing Analysis Methodology.
<br />
<br /> 11.4 Historical Perspective and Related Work.
<br />
<br /> 11.5 Summary.
<br />
<br /> Exercises.
<br />
<br /> 12 OPTIMIZATION OF RULE–BASED SYSTEMS.
<br />
<br /> 12.1 Introduction.
<br />
<br /> 12.2 Background.
<br />
<br /> 12.3 Basic Definitions.
<br />
<br /> 12.4 Optimization Algorithm.
<br />
<br /> 12.5 Experimental Evaluation.
<br />
<br /> 12.6 Comments on Optimization Methods.
<br />
<br /> 12.7 Historical Perspective and Related Work.
<br />
<br /> 12.8 Summary.
<br />
<br /> Exercises.
<br />
<br /> BIBLIOGRAPHY.
<br />
<br /> INDEX.