Ph.D. Thesis, Report LAAS--90215, pages 1-154 pp.. Toulouse, France: Centre National de la Recherche Scientifique, Lab. d'Automatique et d'Analyse des Systemes, 1990. In French.
Abstract: Two main steps in the design of distributed systems are modeling and verification. Petri nets and CCS are two basic formal models. A structuring technique based on CCS concepts is introduced for predicate/transition nets. It consists of a high level petri net that permits expression of communication with value passing. In particular, a petri net composition operator, that can be interpreted as a multi-rendezvous between communicating systems, is defined. The developed formalism is highly convenient for refining abstract models relative to less abstract levels. Based on this work, a software tool, supporting distributed system design and verification, is developed.
Keywords: modelling (and) verification (of) distributed systems (with) labelled predicate/transition net(s); CCS; net composition; rendezvous (between) communicating system(s); refinig.