In the application of the different models, it could be shown that the formalisms of the models, state graph and Petri net, are well applicable in control design. The interrelationships of the processes can be represented very well and a complete overview of the possible states is guaranteed.
In the example, a restriction was made to a sequence control, which made the comparison to the SZM possible. The SZM can be used for sequence controls and describes the control task and the relationships of the input vectors to the states exactly. Each input vector is assigned to a defined diagnostic state, which is displayed on the HMI. High reliability and functionality can be demonstrated through simulation and testing at the SZM.
This can only be achieved to a limited extent on the known models' state graph and Petri net. From the simulation, further definitions must be introduced by the engineer into the formal specification to assign all input vectors to a defined state in the control algorithm. After all forbidden states and transitions have been incorporated, it can be assumed that the control algorithm can interpret all situations. However, the user still has no information about the state and activity of the control.
This must be done by the engineer in a separate work step. In the SZM, these steps are combined and the simulation is used to test the function and prove the reliability. In conclusion, it is obvious that only the method of SZM can solve the complexity of systems that are to be solved with automata. The "state explosion problem" is a limiting one in modelling and its verification. With Selmo, which is based on the SZM, this problem has become manageable.