Contents -- Preface -- Organization of the Monograph -- Dependence of the chapters -- Acknowledgement -- PART I: Real Time Systems - Background -- Summary -- 1 Real Time System Characteristics -- 1.1 Real-time and Reactive Programs -- 2 Formal Program Development Methodologies -- 2.1 Requirement Specification -- 2.1.1 An Example -- 2.2 System Specifications -- 3 Characteristics of Real-Time Languages -- 3.1 Modelling Features of Real-Time Languages -- 3.2 A Look at Classes of Real-Time Languages -- 4 Programming Characteristics of Reactive Systems -- 4.1 Execution of Reactive Programs -- 4.2 Perfect Synchrony Hypothesis -- 4.3 Multiform Notion of Time -- 4.4 Logical Concurrency and Broadcast Communication -- 4.5 Determinism and Causality -- PART II: Synchronous Languages -- Summary -- 5 Esterel Language: Structure -- 5.1 Top Level Structure -- 5.1.1 Signals and Events -- 5.1.2 Module Instantiation -- 5.2 Esterel Statements -- 5.2.1 Data Handling Statements -- 5.2.2 Reactive Statements -- 5.2.3 Derived Statements -- 5.3 Illustrations of Esterel Program Behaviour -- 5.4 Causality Problems -- 5.5 A Historical Perspective -- 6 Program Development in Esterel -- 6.1 A Simulation Environment -- 6.2 Verification Environment -- 7 Programming Controllers in Esterel -- 7.1 Auto Controllers -- 7.1.1 A Very Simple Auto Controller -- 7.1.2 A Complex Controller -- 7.1.3 A Cruise Controller -- 7.1.4 A Train Controller -- 7.1.5 A Mine Pump Controller -- 8 Asynchronous Interaction in Esterel -- 9 Futurebus Arbitration Protocol: A Case Study -- 9.1 Arbitration Process -- 9.2 Abstraction of the Protocol -- 9.3 Solution in Esterel -- 10 Semantics of Esterel -- 10.1 Semantic Structure -- 10.2 Transition Rules -- 10.2.1 Rules for Signal Statement -- 10.3 Illustrative Examples -- 10.4 Discussions -- 10.5 Semantics of Esterel with exec.

PART III: Other Synchronous Languages -- Summary -- 11 Synchronous Language Lustre -- 11.1 An Overview of Lustre -- 11.2 Flows and Streams -- 11.3 Equations, Variables and Expressions -- 11.4 Program Structure -- 11.4.1 Illustrative Example -- 11.5 Arrays in Lustre -- 11.6 Further Examples -- 11.6.1 A Very Simple Auto Controller -- 11.6.2 A Complex Controller -- 11.6.3 A Cruise Controller -- 11.6.4 A Train Controller -- 11.6.5 A Mine Pump Controller -- 12 Modelling Time-Triggered Protocol (TTP) in Lustre -- 12.1 Time-Triggered Protocol -- 12.1.1 Clock Synchronization -- 12.1.2 Bus Guardian . -- 12.2 Modelling TTP in Lustre -- 13 Synchronous Language Argos -- 13.1 Argos Constructs -- 13.2 Illustrative Example -- 13.3 Discussions -- PART IV: Verification of Synchronous Programs -- Summary -- 14 Verification of Esterel Programs -- 14.1 Transition System Based Veri cationy of Esterel Programs -- 14.1.1 Detailed Discussion -- 14.2 Esterel Transition System -- 14.2.1 Abstraction and Hiding -- 14.2.2 Observation Equivalence Reduction -- 14.2.3 Context Filtering -- 14.3 Temporal Logic Based Verification -- 14.4 Observer-based Verification -- 14.5 First Order Logic Based Verification -- 15 Observer Based Verification of Simple Lustre Programs -- 15.1 A Simple Auto Controller -- 15.2 A Complex Controller -- 15.3 A Cruise Controller -- 15.4 A Train Controller -- 15.5 A Mine Pump Controller -- PART V: Integration of Synchrony and Asynchrony -- Summary -- 16 Communicating Reactive Processes -- 16.1 An Overview of CRP -- 16.2 Communicating Reactive Processes: Structure -- 16.2.1 Syntax of CRP -- 16.2.2 Realizing Watchdog Timers in CRP -- 16.3 Behavioural Semantics of CRP -- 16.4 An Illustrative Example: Banker Teller Machine -- 16.5 Implementation of CRP -- 17 Semantics of Communicating Reactive Processes -- 17.1 A Brief Overview of CSP.

17.2 Translation of CSP to CRP -- 17.3 Cooperation of CRP Nodes -- 17.4 Ready-Trace Semantics of CRP -- 17.5 Ready-Trace Semantics of CSP -- 17.5.1 Semantic Definition -- 17.5.2 Semantics of Parallel Composition -- 17.5.3 Semantics of `send' Action -- 17.5.4 Semantics of `receive' Action -- 17.5.5 Semantics of Assignment Statement -- 17.5.6 Semantics of Sequential Composition -- 17.5.7 Semantics of Guarded Selection -- 17.6 Extracting CSP Ready-trace Semantics from CRP Semantics -- 17.6.1 Behavioural Traces of CRP Programs -- 17.7 Correctness of the Translation -- 17.8 Translation into meije Process Calculus -- 18 Communicating Reactive State Machines -- 18.1 CRSM Constructs -- 18.2 Semantics of CRSM -- 19 Multiclock Esterel -- 19.1 Need for a Multiclock Synchronous Paradigm -- 19.2 Informal Introduction -- 19.2.1 Latched Signals -- 19.2.2 Expressions -- 19.2.3 Multiclock Esterel Statements -- 19.2.4 Informal Development of Programs in Multiclock Esterel -- 19.3 Formal Semantics -- 19.3.1 Specification of Clocks -- 19.4 Embedding CRP -- 19.5 Modelling a VHDL Subset -- 19.6 Discussion -- 20 Modelling Real-Time Systems in Esterel -- 20.1 Interpretation of a Global Clock in terms of exec -- 20.2 Modelling Real-Time Requirements in Esterel -- 20.2.1 Deadline Specification -- 20.2.2 Periodic Activities -- 20.2.3 Guaranteed Activities -- 21 Putting it Together -- Bibliography -- Index -- Summary.