OBJSA nets: a class of high-level nets having objects as domains

To define classes of high level nets having structured (individual) tokens is a very fundamental goal for making nets actually usable in real concurrent system modelling. A promising approach is that of combining nets with algebraic specification techniques. This results in a formal specification language which supports both aspects of system modelling, namely data structure and control structure modelling, with suitable abstraction notions. Some different formalisms combining nets and abstract data types have been proposed. In this paper, the authors define a class of high-level Petri nets, namely OBJSA net systems (or OBJSA nets for short), in which: (1) the net can be decomposed into state-machine components, i.e. it preserves the main characteristics of Superposed Automata (SA) nets; (2) the domains to which individual tokens belong are defined as abstract data types by using the language OBJ2. For this class of nets two products (namely an S-product otimes and a T-product odot) are then provided for defining, respectively, the S- and T-invariants as the first step for preserving in the resulting specification language the possibility, typical of nets, of deriving properties of the modelled system by using algebraic techniques