Grosu: Automated refinement checking for asynchronous processes

And/Or Hierarchies and Round Abstraction

Radu Grosu

Sequential and parallel composition are the most fundamental operators for incremental construction of complex concurrent systems. They reflect the temporal and respectively the spatial properties of these systems. Hiding temporal detail like internal computation steps supports temporal scalability and may turn an asynchronous system to a synchronous one. Hiding spatial detail like internal variables supports spatial scalability and may turn a synchronous system to an asynchronous one. In this paper we show on hand of several examples that a language explicitly supporting both sequential and parallel composition operators is a natural setting for designing heterogeneous synchronous and asynchronous systems. The language we use is sHrm, a visual language that backs up the popular and/or hierarchies of statecharts with a well defined compositional semantics.

Proceedings ofthe 25th International Symposium on Mathematical Foundations of Computer Science ( MFCS'00), Bratislava, Slovak Republic, Europe, August 28 - September 1, 2000.