Analysis and Applications of Receptive Safety Properties in Concurrent Systems

Abstract

Formal verification for complex concurrent systesm is a computationally intensive and in some cases, intractable process. The compexity is an inherent part of the verification process due to the system complexity that is an exponential function of the sizes of its components. However, some properties can be enforced by atuomatically synchronizing the components, thus eliminating the need for verfication. Moreover, the complexity of the analysis required to enforce the properties grows incrementally with addition of new components and properties that make the system complexity grow exponentially. The properties in question are the receptive safety properties, a subset of safety properties that can only be violated by component actions. The receptive safety properties represent the realizable subset of the gerneral safety properties because a system that satisfies any non-receptive safety properties mst satisfy related receptive safety properties. This implies that any system with realizable safety requirements can be described as a set of components and receptive safety properties that specify the component interaction that satisfies the requirements. We have developed a methos that automaticaly synchronizes complex concurrent systems to enforce their receptive safety propeties. Many non-safety properties, and automated synchronization can be used to enforce them. (Also cross-referenced as UMIACS-TR-98-11)