Reactive Modules

12 years 6 months ago
Reactive Modules
We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise-re nement) design and veri cation. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a exible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchr...
Rajeev Alur, Thomas A. Henzinger
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1996
Where LICS
Authors Rajeev Alur, Thomas A. Henzinger
Comments (0)