A Unified Framework for Verification and Complexity Analysis of Real-Time and Distributed Systems
Abstract
We have developed the timed I/O automaton model, a basic compositional formal model for describing and analyzing real-time systems and distributed systems (in particular, distributed systems with precise timing sumptions and requirements). We have developed proof techniques, both manual and computer-assisted, for use with timed I/O automata, and have used the model and methods for analyzing a variety of problems and systems. These examples arise from a diverse set of application areas, including connection management protocols, clock synchronization, fault-tolerant distributed consensus, group communication, and real-time process control systems. We have extended the basic timed I/O automaton model in three directions: to include liveness constraints (Live timed I/O automata), hybrid continuous/discrete behavior (hybrid I/O automata), and probabilistic behavior (probabilistic timed I/O automata). In each case, we have developed proof methods and have applied the models and methods to substantial problems. For example, in the hybrid systems area, we have carried out an extended case study of safety aspects of automated transportation systems. We have recently begun the development of a programming language/environment, based upon our formal models, and intended to support the coordinated development and analysis of distributed systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 13, 1997
- Accession Number
- ADA332549
Entities
People
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology