Alur, Rajeev; Henzinger, Thomas AIST Austria
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-refinement) design and verification. 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 flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single 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 synchronous message-passing protocols.
Formal Methods in System Design
7 - 48
Alur R, Henzinger TA. Reactive modules. Formal Methods in System Design. 1999;15(1):7-48. doi:10.1023/A:1008739929481
Alur, R., & Henzinger, T. A. (1999). Reactive modules. Formal Methods in System Design. Springer. https://doi.org/10.1023/A:1008739929481
Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” Formal Methods in System Design. Springer, 1999. https://doi.org/10.1023/A:1008739929481.
R. Alur and T. A. Henzinger, “Reactive modules,” Formal Methods in System Design, vol. 15, no. 1. Springer, pp. 7–48, 1999.
Alur R, Henzinger TA. 1999. Reactive modules. Formal Methods in System Design. 15(1), 7–48.
Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” Formal Methods in System Design, vol. 15, no. 1, Springer, 1999, pp. 7–48, doi:10.1023/A:1008739929481.