Accession Number : ADA332549
Title : A Unified Framework for Verification and Complexity Analysis of Real-Time and Distributed Systems
Descriptive Note : Final technical rept. Aug 93-Feb 97
Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE
Personal Author(s) : Lynch, Nancy
PDF Url : ADA332549
Report Date : 13 JUN 1997
Pagination or Media Count : 57
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.
Descriptors : *DISTRIBUTED DATA PROCESSING, SOFTWARE ENGINEERING, COMPUTER COMMUNICATIONS, REAL TIME, PROGRAMMING LANGUAGES, INPUT OUTPUT PROCESSING, SYNCHRONIZATION(ELECTRONICS), HYBRID SYSTEMS, COMPUTER PROGRAM VERIFICATION, AUTOMATA.
Subject Categories : Computer Systems
Distribution Statement : APPROVED FOR PUBLIC RELEASE