Automated Computation of Decomposable Synchronization Conditions

dc.contributor.authorMatos, Gilbertoen_US
dc.contributor.authorPurtilo, James M.en_US
dc.contributor.authorWhite, Elizabethen_US
dc.description.abstractThe most important aspect of concurrent and distributed computation is the interaction between system components. Integration of components into a system requires some synchronization that prevents the components from interacting in ways that may endanger the system users, its correctness or performance. The undesirable interactions are usually described using temporal logic, or safety and liveness assertions. Automated synthesis of synchronization conditions is a portable alternative to the manual design of system synchronization, and it is already widespread in the hardware CAD domain. The automated synchronization for concurrent software systems is hindered by their excessive complexity, because their state spaces can rarely be exhaustively analyzed to compute the synchronization conditions. The analysis of global state spaces is required for liveness and real--time properties, but simple safety rules depend only on the referenced components and not on the rest of the system or its environment. Synchronization conditions for delayable safety critical systems can be computed without the state space analysis, and decomposed into single component synchronization conditions. Automated synthesis of decomposable synchronization conditions provides a solid groundwork for the independent design of system components, and supports reuse and maintenance in concurrent software systems. This approach to integration of concurrent systems is embodied by GenEx, an analysis and synchronization tool that integrates system components to satisfy a given set of safety rules, and produces executable systems. (Also cross-referenced as UMIACS-TR-97-10)en_US
dc.format.extent440179 bytes
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
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3748en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-97-10en_US
dc.titleAutomated Computation of Decomposable Synchronization Conditionsen_US
dc.typeTechnical Reporten_US


Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
429.86 KB
Postscript Files
Thumbnail Image
327.5 KB
Adobe Portable Document Format
Auto-generated copy of