SEGRAS—a formal and semigraphical language combining Petri nets and abstract data types for the specification of distributed systems

Abstract

SEGRAS is formal language for writing and analyzing specifications of distributed software systems. It unifies algebraic specifications of abstract data types with high-level Petri net specifications of nonsequential systems in a common syntactic and semantic framework. The data structure of a system, the information content of its local states, and static constraints to state changes are specified algebraically using positive conditional equations. Dynamic behavior is specified by high level Petri nets. Each net defines a (distributed) initial state and a partial ordering in which state changing operations may happen. SEGRAS addresses advanced programming methodologies by offering facilities for modularization and parameterization, and a type system which supports polymorphism with dependent types, higher-order types, subtypes, and overloading. Some examples are given to illustrate these language concepts.