ISSN:
1572-8102
Keywords:
modeling of reactive systems
;
formal verification
;
compositionality
;
concurrency modeling
;
synchrony and asynchrony
;
assume-guarantee reasoning
;
temporal abstraction
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1008739929481
Permalink
