Specification and Verification of Networks in a Petri Net based Language

Abstract

In this paper we present a system description language and a technique of top-down specification and verification of distributed systems. Our language is called Epsilon, and it has been developed for the description and analysis of systems containing concurrent components.

We have used and developed concepts from the Simula and Delta languages and from Petri net theory. A system described in Epsilon consists of a number of concurrent objects. Each object has a set of attributes, e.g. variables and procedures, and executes a sequence of actions. Epsilon includes both normal algorithmic statements and first order predicate logic as description elements.

An abbreviated version of this paper has been presented at the third European Workshop on Applications and Theory of Petri Nets, Springer Informatik Fachberichte 66.