ACCESS - Algebraic Concurrent Events for System Specification

Access is a new algebraic specification formalism, which focuses on the fine description of the ``true'' concurrency and on a high degree of expressivity. Systems are specified by a set of local states, whose value changes under the occurrence of events. Both events and data structure are specified by abstract data types. Static properties, i.e. global constraints over events and data structure, are described by first order formulae, while dynamic axioms, explaining the behavior of events, are given by causality rules. Concurrency can be described in different ways, it can be interleaving or true concurrency. Finally, expressivity is given by fine descriptions of both static and dynamic properties. Access has demonstrate to be a natural generalization of a great variety of Petri Nets (as for example -Algebraic, -Coloured, -With arc extensions Petri Nets). It is also able to capture concepts from other formalisms as Gamma language or CO-OPN. This report presents a complete description of Access syntax and semantics, together with an example of Access specification based on Petri Nets with Arc Extensions. This report also explains how specifications written in other languages as Petri Nets, Gamma, CO-OPN, are written in Access.