A Unified Framework for Verification and Complexity Analysis of Real-Time and Distributed Systems

点击翻译按钮获取中文摘要

The goal of this project is to define a general formal model for reasoning about real-time and distributed systems, and to establish its value by using it for a variety of purposes. Many models have been proposed for such systems; this project is unique in that it attempts to define a single model that can be used for many different purposes. The uses for such a model include: (1) proving fundamental results about the capabilities of real-time and distributed systems. These include upper and lower bound complexity results (for time, space and communication complexity) and impossibility results: (2) describing real systems, using appropriate programming languages; (3) specifying allowable system behavior; (4) verifying (by hand or by machine) the correctness of algorithms and systems. There are different styles of verification, of which assertional, algebraic and temporal logic methods are probably the most significant; and (5) analyzing system performance. Traditionally, research in each of these areas has been based on a semantic model designed specifically for that area. In contrast, this project aims to conduct work in these areas in terms of a common model. The project focuses particularly on real-time and other timing-based systems (e.g., communication systems and real-time process control systems).