Refinement in a concurrent, object-based language

Abstract

Nonsequential automata constitute a categoria! semantic domain based oo labeled transition system with full concurrency, where restriction and relabeling are functorial and a class oi morphisms stands for refinement. It is, for ou r knowledge, the first model for concurrency which satisfies the diagonal compositionality requirement, i.e., refinements compose (vertical) and distribute over combinators (horizontal). To experiment with the proposed semantic domain, a semantics for a concurrent, object-based language is given. lt is a simplified and revised version oi lhe object-oriented specification language GNOME, introducing sane special features inspired by lhe semantic domain such as refinement. The diagonal compositionality is an essential property to give semantics in this context.