Automated Computation of Decomposable Synchronization Conditions
Automated Computation of Decomposable Synchronization Conditions
Loading...
Files
Publication or External Link
Date
1998-10-15
Authors
Matos, Gilberto
Purtilo, James M.
White, Elizabeth
Advisor
Citation
DRUM DOI
Abstract
The 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)