Review: Modular Formalism, with Petri Nets (1978)

A review of the research paper:

"Top-Down Formal Specification and Verification of Parallel Control Systems"
by R. Valette, and M. Diaz
in Digital Processes, vol:4, 1978, pp.181-199


VD78 introduces a methodology to model, and seamlessly verify,

in an easy way the communications and synchronizations in distributed control systems.
(VD78, p.181)

Legitimate Heir

VD78 does not introduce new graph types. It orchestrates the prior art, to found a feasible methodology.

The approach presented in this paper consists of three levels of validation:

- level 1 applies only at the control structure of the system, this control structure being modellized by a Petri net which allows the check of safeness, liveness, etc. Note that this approach is not possible with models such as the "organiphase" [5], where the control graph needs an interpretation to represent a scheduling,

- level 2 applies at the level constituted by the control structure and the data graph which is able to check the determinism and determinacy; at this level the predicates and actions are not specified in a precise way,

- level 3 applies at the whole system, when the predicates and actions are specified. The formal proof is done by using assertions [6]. This level is the classical one that is usually used in proving correctness of programs [7-8].

(VD78, p.182, emphasis-added)

VD78 keeps Petri nets as it is, for the first level, although avoids some patterns of the regular Petri net use. Instead, VD78 suggests the data-graph (after LOGOS), to represent unbounded variables, and whatever pertains to data. The Petri net is used for control of (the structure of) events. The (internal) computations are in its data-graph.

At the second level, VD78 lets associate a label with any Petri net transition, through a label to point at its data-graph. A label lists the related data-operator and/or the data-predicate - to avoid, non-determinacy (race-conditions), and/or non-determinism, respectively.

The third level is not published in VD78, but it is available in Va76, the Ph.D. of Valette (in French). VD78 reasons that, the interest of the method is the ease, provided by the first two levels, to the third - by pre-verifying the system structure.

Ready-Modularity, with Well-Formed subnets

With VD78, to model, is together, at every turn, with the verifier. This contrasts, for example, with a strategy to model the net first, whether module-by-module or as a single piece, only next, to verify all of it, together (such as with SARA). For this ready-modularity,

Definition: Let P be a Petri net safe for an initial marking M0. P is said to be "well-formed" for M0 iff the three following conditions are verified:

1. P is live for M0,
2. P has a special place, called the "idle" place such that:
- this place has one and only one successor transition called "initial" transition.
- this place has one and only one predecessor transition called "final" transition.
3. M0 is the only marking of the forward marking class F(M0) for which the "idle" place has a token and the only transition enabled by M0 is the "initial" transition.

(VD78, p.189, emphasis added, and F(M0) is a font-replacement.)

That "idle" place represents the rest of the net, as referrable by the well-formed subnet. To use Petri net terms, the net and the well-formed subnet, are represented to each other, as a Petri net place vs. a Petri net transition, respectively.

Further Reading

Some readers may question whether the well-formedness restrictions of VD78 are "too restrictive." i.e: May it not be defined in some other way? Maybe. But you should first appreciate the elegance of VD78, before you "challenge" it, or else, you may be only to commit to a worse than trivial junk, such as copycat82, which claims to "let" arbitrary dissections of a net, but it is not verifiable, any more, although it attempts to! That is, copycat82 is fault-prone, in its ignorance.

copycat82, is a subset of VD78, as copycat82 commits plagiarism, and its sheer ignorance, and/or immense neglect, provides a lot of un-exemplar examples, to avoid, when working with net-formalisms.

Forum: . . (Fair Menu . . . . . Fault Report? . . . . . Remedy for your case . . . . . Noticed Plagiarism?)

Referring#: 0.0.1
Last-Revised (text) on Oct. 23, 2004
(revised presentation/link, on Nov. 6, 2004) . . . published as
Written by: Ahmed Ferzan/Ferzen R Midyat-Zila (or, Earth)
Copyright (c) [2002,] 2004, 2009 Ferzan Midyat. All rights reserved.