The Verification of Inter-Locking Specification by Petri Nets


Hiroshi FUKUOKA, Mitsuyoshi FUKUDA
This paper describes how to verify an inter-locking specification by a formal method and Petri Nets. We made a formal specification of an inter-locking system in Z specification Language from a traditional (informal) specification. Then, we translated the Z specification into a Petri Nets. We think that it is easy to automate most of these procedures. To verify the specification written in Petri Nets, we developed a verification system which tests the reachability, a verification measure of a Petri Nets method.