Modular algebraic nets to specify concurrent systems

Abstract

The authors present the basic features of a specification language for concurrent distributed systems, developed at the Department of Information Sciences of the University of Milan, Italy. The language is based on a class of modular algebraic high-level nets, OBJSA nets, which result from the synthesis of superposed automata (SA) nets and of the algebraic specification language OBJ. It is supported by the OBJSA Net Environment (ONE). OBJSA nets stress the possibility of building the system model by composing its components and encourage the incremental development of the specification and its reusability. An OBJSA net consists of an SA net inscribed with terms of an OBJ module. The ONE environment supports the user in producing and executing a specification, hiding from her/him, as much as possible, the technical details of the algebraic part of the specification. The paper provides a complete presentation of OBJSA nets, including a user-oriented introduction, the definition of OBJSA nets (as subclass of SPEC-inscribed nets), of their occurrence rule (the semantics) and of the composition operation. In addition it presents the kernel of the support environment.