Real-Time Systems

The following sections are included:

• Preface

• Contents

The following sections are included:

• Introduction

• Time and Events

• Discrete Real-Time Systems

• Composition and Decomposition of iDRTS Structures

• DRTS as Algebras

• A Model for Sequential Processes

• Conclusions

The following sections are included:

• Introduction: Real-Time and Reactive Systems

• Reactive Programming: Asynchronism versus Strong Synchronism

• The Weak Synchronous Paradigm

• COREA: A Weak Synchronous Process Algebra
  • Abstract Syntax
  • Weak Synchronous Operational Semantics
    • Transition
    • Inaction
    • Case
    • Concurrency
    • Recursion
  • Congruence
  • Equational Laws
  • Brief Comparison with CCS

• Application to Distributed Reactive Programming
  • ESTEREL: Brief Overview
  • ɛC = ESTEREL + COREA

• Towards Weak Synchronous Distributed Implementations
  • (f) Protocol SB (Single Bus)

• Application to Embedded Systems

• Conclusion

We present a model of probabilistic processes, which is an extension of CSP, on the basis of replacing internal non-determinism by generative probabilistic choices, and external non-determinism by reactive probabilistic choices. Our purpose when defining the model has been to maintain, as far as possible, the meaning of all the operators in classical CSP, generalizing them in a probabilistic way. Thus we try to keep valid (once probabilistically generalized), as far as possible, the laws of CSP. It is the combination of both internal and external choice that makes strongly difficult the definition of a probabilistic version of CSP. We can find in the literature quite a number of papers on probabilistic processes, but only in a few of them internal and external choices are combined trying to preserve their original meaning. The denotational semantics here presented is based on a domain of probabilistic trees with two kinds of nodes, representing the internal and external choices, the root being an internal one, which generalizes in a very natural way the corresponding trees for nonprobabilistic process algebras. We present also a testing semantics fully abstract with respect to our denotational semantics.

The following sections are included:

• Introduction

• Grafcet
  • Graphical Elements
  • Temporal Aspect
  • Evolution Rules and Interpretation

• First Modeling
  • Transition System
  • Synchronization Constraints
  • Temporization
  • Limits

• Second Modeling
  • Construction of Basic Transition Systems
  • Building of the Global Transition System

• Proof
  • Second Modeling
  • First Modeling

• Example and Results
  • Example
  • Results

• Conclusion

The following sections are included:

• Introduction

• Preliminaries
  • A Short Description of µCRL
  • Linear Process Operators
  • Internal Actions

• Sufficient Conditions for the Equality of LPOs

• Abstraction and Idle Loops

• Examples
  • The Concurrent Alternating Bit Protocol
    • Specification
    • Expansion
    • Invariant
    • Abstraction and focus points

It is important to verify timing conditions in real-time systems. The verification methods such as model checking and language inclusion algorithm, bisimulation method have been researched. Especially symbolic model checking is promising for verifying a large system. Time models are classified into discrete time model and dense time model. In discrete time model, symbolic model checker based on BDDs (Binary Decision Diagrams) has been developed. But in dense time model, symbolic model checking based on BDDs causes the state-explosion problem because of generating region graph from specification. In this chapter, we propose symbolic model checking based on BDDs in dense time model, which do not use region graph. In our proposed symbolic model checker, we represent state spaces by both BDDs and DBMs (Difference Bound Matrices). We have realized effective symbolic model checker based on BDDs in dense time model by proposed method.

The following sections are included:

• Introduction

• The Circal Process Algebra
  • Informal Semantics
  • Formal Semantics

• The Methodology

• Constraint-Based Modeling

• A Temporal Logic for Simultaneous Actions

• The Representation of Properties
  • Formula-Based Characterization
  • Model-Based Characterization

• Discussion and Future Work

The TTM/RTTL framework allows for the specification, development and verification of discrete real-time properties of reactive systems. Timed transition systems (TTMs) is the underlying computational model, and real-time temporal logic (RTTL) is the requirements specification language. In this paper, we provide a conversion procedure for mapping a timed transition system into a finite state fair transition systems. This means that efficient (untimed) tools for state exploration can be used to check the properties of real-time systems. The procedure has been implemented in the Statetime toolset for the TTM/RTTL framework.

Synthesis approaches involve deriving a program from a high-level specification. This can be accomplished by using synthesis algorithms that are well adapted to a particular application domain. Efficiency of synthesis algorithms may be demonstrated by experiments done in different settings. Such experiments help to bridge the gap between empirical practices and formal methods. We present an academic experiment that constitutes a first step toward the performance study of synthesis algorithms that allow verification of properties while generating controllers for discrete-event systems. The goal of this experiment is to show the limitations of synthesis algorithms and compare algorithms between them.

The following sections are included:

• Introduction

• Syntax

• Operational Semantics

• Testing Semantics

• Operational Characterization
  • Sets of States
  • States of a Process
  • Barbs

• Congruence

• Conclusions and Future Work

The following sections are included:

• Introduction

• Graphical Temporal Representation

• Interprocess Communication
  • Interprocess I/O Operators
  • Interprocess Composition Operators
  • Synchronous and Asynchronous Operators

• Composition of Temporal and Interprocess Models
  • Syntax of the Compositional Model
  • Temporal Semantics of the Compositional Model
  • Operational Semantics of the Compositional Model
  • The Simulation of an Inspection Station

• Time Extended LOTOS
  • Operational Semantics of Time Extended LOTOS
  • Conversion Rules among LOTOS Operands and Interprocess Composition Operands
  • The Conversion of the Inspection Station Example

• Related Work

• Conclusions and Further Work

The Ramon Llull Environment (RALE), a development environment for parallel-distributed (PD) and real-time (RT) software, is reported. It has been developed with didactic and industrial concerns, and with integrating and unifying aims. This effort has resulted in a novel language, PADD, and in an integrated set of tools for both teaching concurrency and parallelism, and for developing real-life systems. The explicit character of parallelism in PADD allows the definition of hardware high-level models in addition to software. Extensive application of tree-like schemes for the user interface and to represent PADD programs, the introduction and usage for system refinement of the concept of Communication-extended Abstract Types (CATs), monitor elimination and communication elimination transformations, and their integration with simulation, allocation-mapping, and documentation generation tools are amongst the elements integrated within the environment. Its cooperation with well established specification and verification environments for concurrent programs is under investigation.

The following sections are included:

• Introduction

• Object-Interaction Models

• Object-Behavior Models

• Object-Relationship Model

• Tunable Formalism

• State of OSA

• Conclusion

The following sections are included:

• Introduction

• Algebraic Specification of CTL

• Algebraic Implementation of a Model Checker
  • Structure of an Algebraic Compiler
  • The Macro Processor Generating Satisfiability Sets
  • Generating a Model Checker Program
  • Implementing the Macro Processor

• Conclusions

The following sections are included:

• Introduction

• Related Work

• Example

• Our Framework
  • Elementary Processes
  • Composition Operators

• Synthesis Example

• Conclusion

The following sections are included:

• Introduction

• Hybrid Input/Output Automata

• Mathematical Preliminaries
  • Assumptions about the Constants
  • Some Useful Functions
    • Function f
    • Function g
    • Function f₁
    • Function h

• High Level Specification V
  • Overview
  • Formal Description

• Derivative Automaton D
  • Formal Description
  • Some Properties of D
  • D Implements V
  • An Approximate Result

• Modifications to V and D to Incorporate Periodic Feedback
  • Modified High Level Specification V₁
  • Modified Derivative Automaton D₁
  • Modified Correctness Proof

• The Implementation Impl
  • Vehicle
  • Controller
  • Impl
  • Impl Implements D₁

• Discussion

The following sections are included:

• Introduction

• Timing Diagram Specifications

• Causal Partitions over TD Specifications

• Compatibility of Realizable Timing Diagrams

• Extension to Cyclic Behaviors

• Conclusions

The following sections are included:

• Introduction

• The Experiment Context
  • The Modulor Project
  • Analyzed Mechanisms and Their Properties
  • Targeted Experiments

• Synchronization Validation with Spin
  • Promela
  • Specification of the Particular Case
  • Generalization
  • Properties
  • Verification

• The Analysis of the Detection Mechanisms
  • Validation of the Communication Strategy with Spin
    • Specification
    • Properties and Verification
  • Validation of the Local Detection with Kronos
    • Timed Automata
    • Specification
    • Properties
    • Verification

• Discussion

Multi-level data security is a requirement in many of today's advanced, real-time embedded systems. Current approaches to meeting multi-level security requirements are based on expensive custom or proprietary hardware and software. However, real-time embedded systems are evolving towards open-system architectures and commercial off-the-shelf (COTS) hardware and software. It is therefore important to develop a standard method for evaluating the security aspects of real-time embedded systems, and for handling black-box COTS components in proprietary systems. This chapter presents a brief analysis of multi-level data security in the context of a simplified exemplary real-time, embedded avionics system and discusses mechanisms that can be used to solve the problem of integrating COTS components into a secure system. As is required of high assurance secure systems, a formal model of one such mechanism based on the use of a trusted network interface unit mechanism is provided using the LOTOS formal specification language.

The following sections are included:

• Motivation and Background

• Basic Concepts and Notation

• A Method for Analyzing and Detecting Feature Interactions
  • Specification of Features in the Context of a System (Step 1)
  • Integration versus Composition of Features (Steps 2 and 3)
  • Derivation of Test Cases to Detect Interactions (Step 4)
  • Executing the System and Analysing the Results (Steps 5 and 6)

• Conclusions and Research Directions

The following sections are included:

• Appendix A Algebraic Specification

• Bibliography

• Index