Rapporto Interno No. 89-004, pages 1-55 pp.. Politecnico Di Milano (Italy), 1989.
Abstract: In this paper, the authors define a method for symbolic execution of concurrent systems, based on an extension of the Petri net formalism, called EF nets. Depending on the level of abstraction of actions and predicates that one associates to the transitions of the net, EF nets can be used as a high-level specification formalism for concurrent programs. In the paper in order to support the analysis of a concurrent system or program, at first a general algorithm for symbolically executing an EF net is defined. Then, a more efficient algorithm is given for the particular, though important, subclass of 1-safe EF nets, which can be extended to bounded EF nets. Such algorithm is proved to significantly help in reducing the amount of information needed to characterize a symbolic execution.
Keywords: symbolic execution (of) concurrent program (using nets); EF net; extended net; high-level specification (for) concurrent program; safe EF net; bounded EF net.