Each chapter, derived from papers presented at the all-invitation 1st AMAST International Workshop on Real-Time Systems (Iowa, 1993), is written by leaders in their field. The chapters form an intriguing mix of modeling, specification, verification, and implementation of "real" real-time systems. They cover untimed and timed systems, sequential, concurrent and embedded real-time processes, integrated models using state machines, temporal logic and algebraic data models, real-time CSP, verification tools, system design using temporal logic, symbolic checking of discrete time models, iterative symbolic approximation in timing verification and verification of audio protocols, timed full LOTOS and timed LOTOS extensions, LOTOS specification of telephone services and flight warning computers, and performance analysis.

Contents:

• Real-Time System = Discrete System + Clock Variables
• Real-Time CSP
• Visual Tools for Verifying Real-Time Systems
• Designing Supervisors for Real-Time Systems
• Real-Time Symbolic Model Checking for Discrete Time Models
• Verification of an Audio Control Protocol
• Approximations for Verifying Timing Properties
• A Timed Full LOTOS with Time/Action Tree Semantics
• A Timed LOTOS Extension
• Status-Oriented Telephone Service Specification
• Experimenting with LOTOS in the Aerospace Industry
• Performance Analysis and True Concurrency Semantics
• State Machines, Temporal Logic and Algebraic Data Models
• An Experiment in Developing Real-Time Systems Using Mec

"... an interesting combination of papers devoted to the formal specification and verification of real-time systems. The diversity of approaches and the treatment of the subject from various angles work very much in its favour ... recommend the book to anyone interested in the formal description of real-time systems' behavior."