Formal modeling and verification of a part manufacturing systems using FSZ-automaton with CLS criteria

摘要

Failures in manufacturing systems reliant on human operators must address the issues of coverage, liveness, and starvation (CLS) to prevent accidental interactions among the component of the system or accidental human-automation interaction (HAI). Manufacturing systems would benefit from techniques that lay the ground work for investigating the possible rectifications for problems that might cause down time. The formal verification is the dominant technique utilized, along with mathematical proof that shows that an accordingly scaled model of a manufacturing system contains the desired properties of the large real-world manufacturing systems. This paper describes a method of FSZ-automaton, which combines finite-state machine model with Z-schemas for establishing concurrency and a distributed structure within manufacturing systems. FSZ-automaton was used to complete the formal verification of the part manufacturing system. This formal verification is also used to validate FSZ-automaton, its usability properties, and to distinguish the mode confusion. Moreover, the advances in formal verification continue to address these issues, such that the traditional analysis procedure is validated and can potentially avoid this constraint.