Show simple item record

Analysis and Applications of Receptive Safety Properties in Concurrent Systems

dc.contributor.authorMatos, Gilbertoen_US
dc.description.abstractFormal 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)en_US
dc.format.extent822770 bytes
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3874en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-98-11en_US
dc.titleAnalysis and Applications of Receptive Safety Properties in Concurrent Systemsen_US
dc.typeTechnical Reporten_US
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtUMIACS Technical Reportsen_US

Files in this item


This item appears in the following Collection(s)

Show simple item record