Self-checking implementation of Boolean interpreted Petri nets

This paper presents a technique of constructing a self-checking synchronous implementation of a Boolean interpreted Petri net. The validated Petri net specification is modeled with a circuit that automatically detects faults visible at Petri net level. The so called direct approach is used in modeling Petri nets by hardware. The faults that can be checked at hardware level manifest themselves at Petri net level through entering markings that do not belong to the set of allowable ones. These markings violate certain P-invariant assertions. A hardware framework based on self-checking checkers that allows detecting the violation of the P-invariant assertion is proposed.<>