Analysis and Applications of Receptive Safety Properties in Concurrent
Systems
Analysis and Applications of Receptive Safety Properties in Concurrent
Systems
Files
Publication or External Link
Date
1998-10-15
Authors
Matos, Gilberto
Advisor
Citation
DRUM DOI
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)