Analysis and Applications of Receptive Safety Properties in Concurrent Systems
Abstract
Formal verification for complex concurrent systems is a computationally intensive and, in some cases, intractable process. The complexity 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 automatically synchronizing the components, thus eliminating the need for verification. 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 general safety properties because a system that satisfies any non-receptive safety properties must 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 method that automatically synchronizes complex concurrent systems to enforce their receptive safety properties. Many non-safety and non-receptive properties can be represented using receptive safety properties, and automated synchronization can be used to enforce them.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1998
- Accession Number
- ADA356803
Entities
People
- Gilberto Matos
Organizations
- University of Maryland