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 VariablesReal-Time CSPVisual Tools for Verifying Real-Time SystemsDesigning Supervisors for Real-Time SystemsReal-Time Symbolic Model Checking for Discrete Time ModelsVerification of an Audio Control ProtocolApproximations for Verifying Timing PropertiesA Timed Full LOTOS with Time/Action Tree SemanticsA Timed LOTOS ExtensionStatus-Oriented Telephone Service SpecificationExperimenting with LOTOS in the Aerospace IndustryPerformance Analysis and True Concurrency SemanticsState Machines, Temporal Logic and Algebraic Data ModelsAn Experiment in Developing Real-Time Systems Using Mec
Readership: Computer scientists and software engineers.
keywords:System, Time;Temporal Logic;Real Time System;Verification;Model Checking;Symbolic Model Checking;Control Protocol;Timing Properties;Performance Analysis;LOTOS;LOTOS Extension;State Machine;Visual Tools;Supervisory Tools;MEC System
“… 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.”Control Engineering Practice