Real Time Programming: Languages, Specification and Verification

The following sections are included:

• Preface

• Acknowledgement

• Contents

In the next four sections, we shall provide (i) an overview of the general characteristics of real-time systems and reactive systems, (ii) a general discussion on formal development methodologies for real-time systems, (iii) characteristics of real-time languages and (iv) programming characteristics of reactive systems and the synchrony hypothesis.

The following sections are included:

• Real-time and Reactive Programs

The following sections are included:

• Requirement Specification
  • An Example

• System Specifications

The following sections are included:

• Modelling Features of Real-Time Languages

• A Look at Classes of Real-Time Languages

The following sections are included:

• Execution of Reactive Programs

• Perfect Synchrony Hypothesis

• Multiform Notion of Time

• Logical Concurrency and Broadcast Communication

• Determinism and Causality

Several synchronous languages have been proposed in the literature. The principal languages of the family of synchronous languages that have been founded on the perfect synchrony hypothesis are ESTEREL, LUSTRE and SIGNAL. ESTEREL is an imperative language that has its origin in catering to explicit control applications. LUSTRE has been founded on a data flow model, whereas SIGNAL is a relational model that has its origin in the specification of feedback control systems. In a sense all these languages are equally powerful with the exception that SIGNAL is more expressive from the specification point of view. Statecharts is a visual formalism that can in fact be included in the family of synchronous languages considered from the perspective of specifying robust reactive systems. Statcharts are not strictly based on the synchrony hypothesis even though formally it has been defined with respect to asynchronous and synchronous models. Argos is another synchronous language that is based on visual formalism similar to Statecharts based on synchrony hypothesis. It must be noted that all these languages have found significant usage in various industries like Avionics, CAD, Nuclear plant control, Telecom, Automobile etc. In this part (next six chapters), we shall discuss the following languages structure, methodology, semantics and programming of typical reactive real-time systems in ESTEREL.

The following sections are included:

• Top Level Structure
  • Signals and Events
  • Module Instantiation

• ESTEREL Statements
  • Data Handling Statements
  • Reactive Statements
  • Derived Statements

• Illustrations of ESTEREL Program Behaviour

• Causality Problems

• A Historical Perspective

The following sections are included:

• A Simulation Environment

• Verification Environment

The following sections are included:

• Auto Controllers
  • A Very Simple Auto Controller
  • A Complex Controller
  • A Cruise Controller
  • A Train Controller
  • A Mine Pump Controller

In ESTEREL, computations that take time are modeled as tasks; that is, there is non zero time between initiation and completion of a task. In the terminology of ESTEREL, this means that there will be at least one instant between initiation and completion. The exec constructs of ESTEREL is used to initiate the tasks and thus, form asynchronous gateway…

The following sections are included:

• Arbitration Process

• Abstraction of the Protocol

• Solution in ESTEREL

The following sections are included:

• Semantic Structure

• Transition Rules
  • Rules for Signal Statement

• Illustrative Examples

• Discussions

• Semantics of Esterel with exec

In the the next two chapters, we shall provide an overview of Lustre- a dataflow synchronous programming language (based the dataflow language Lucid) and Argos derived from the Statechart graphical formalism.

The following sections are included:

• An Overview of LUSTRE

• Flows and Streams

• Equations, Variables and Expressions

• Program Structure
  • Illustrative Example

• Arrays in LUSTRE

• Further Examples
  • A Very Simple Auto Controller
  • A Complex Controller
  • A Cruise Controller
  • A Train Controller
  • A Mine Pump Controller

The following sections are included:

• Time-Triggered Protocol
  • Clock Synchronization
  • Bus Guardian

• Modelling TTP in LUSTRE

The following sections are included:

• ARGOS Constructs

• Illustrative Example

• Discussions

In this part, we will describe important approaches that are used for the verification of programs in synchronous languages like ESTEREL, and Lustre. First we will discuss in detail the verification approaches used for verification of ESTEREL programs. This will be followed by an illustration of verification techniques for LUSTRE programs.

The following sections are included:

• Transition System Based Verification of ESTEREL Programs
  • Detailed Discussion

• ESTEREL Transition System
  • Abstraction and Hiding
  • Observation Equivalence Reduction
  • Context Filtering

• Temporal Logic Based Verification

• Observer-based Verification

• First Order Logic Based Verification

The following sections are included:

• A Simple Auto Controller

• A Complex Controller

• A Cruise Controller

• A Train Controller

• A Mine Pump Controller

Programming languages that have been used for real-time programming can be broadly categorized into:

1. Asynchronous Languages: Here, a program is treated as a set of loosely coupled independent execution units or processes, each process evolving at its own pace. Interprocess communication is done by mechanisms such as message passing. Communication as a whole is asynchronous in the sense that an arbitrary amount of time can pass between the desire of communication and its actual completion. This class includes languages such as Ada, Occam, CSP etc.

2. Perfectly Synchronous Languages: In this class, programs react instantaneously to its inputs by producing the required outputs. Statements evolve in a tightly coupled input-driven way deterministically and communication is done by instantaneous broadcast where the receiver receives a message exactly at the time it is sent. That is, a perfectly synchronous program produces its outputs from its input with no observable time delay. Languages such as Esterel [12], Lustre, Signal, Statecharts belong to this category. These languages are often referred to as reactive languages. These languages use the multiform notion of time rather than clock time…

The following sections are included:

• An Overview of CRP

• Communicating Reactive Processes: Structure
  • Syntax of CRP
  • Realizing Watchdog Timers in CRP

• Behavioural Semantics of CRP

• An Illustrative Example: Banker Teller Machine

• Implementation of CRP

The following sections are included:

• A Brief Overview of CSP

• Translation of CSP to CRP

• Cooperation of CRP Nodes

• Ready-Trace Semantics of CRP

• Ready-Trace Semantics of CSP
  • Semantic Definition
  • Semantics of Parallel Composition
  • Semantics of 'send' Action
  • Semantics of 'receive' Action
  • Semantics of Assignment Statement
  • Semantics of Sequential Composition
  • Semantics of Guarded Selection

• Extracting CSP Ready-trace Semantics from CRP Semantics
  • Behavioural Traces of CRP Programs

• Correctness of the Translation

• Translation into MEIJE Process Calculus

The following sections are included:

• CRSM Constructs

• Semantics of CRSM

The following sections are included:

• Need for a Multiclock Synchronous Paradigm

• Informal Introduction
  • Latched Signals
  • Expressions
  • Multiclock ESTEREL Statements
  • Informal Development of Programs in Multiclock ESTEREL

• Formal Semantics
  • Specification of Clocks

• Embedding CRP

• Modelling a VHDL Subset

• Discussion

The following sections are included:

• Interpretation of a Global Clock in terms of exec

• Modelling Real-Time Requirements in ESTEREL
  • Deadline Specification
  • Periodic Activities
  • Guaranteed Activities

Language methodologies for specifying and analyzing complex real-time systems has been a challenging issue for quite some time. There have been several approaches for the same. In this monograph, we have primarily focussed on one of the most successful approaches for the design of complex reactive systems: the synchronous approach to reactive/real-time systems…

The following sections are included:

• Bibliography

• Index