Specification/Verification of Temporal Properties for Distributed Systems: Issues and Approaches. Volume 1.

摘要

This report identifies problems, models and solutions in the area of specification and verification of temporal properties for secure distribution systems. The temporal properties studied are security, progress, determinism, and real-time requirements. Also included is work on the specification of fault tolerance and adaptive security policies. The effort is a first look at these issues. The model of a distributed system that will be used in this report is a collection of objects that interact only by passing messages. The only state global to two or more objects is the communication channels that connect them. Every piece of data must be contained in one of the objects and cannot be directly read from another. This model fits very well with a multicomputer, in which there is no memory shared between the nodes, and the objects can be distributed arbitrarily among the nodes. However, it can also be used when objects share a node and some global memory. (kr)