Model Checking in Parallel Logic Controllers Design and Verification

The parallel logic controllers (PLC) developing process can be both, simplified and improved by means of formal methods. The paper presents approach based on Petri nets specification and model checking techniques used for formal verification, synthesis and implementation. Interpreted petri net (IPN) is selected as a formal behavioural model for parallel logic controllers. It is proposed to use graphical modelling tools for formal behavioural PLC modelling, authors ICPN is such example. The use of common standard, like Petri Net Markup Language (PNML) enables integration with formal analysis tools. The model is simplified (optimised) by means of formal reasoning system (Gentzen). The transformation of the simplified model is made automatically into VHDL description and NuSMV model. The resulting VHLD model can be used for simulation and next for synthesis and implementation. The reliability of the PLC is improved by formal verification. The paper presents the application of the additional specification described in the temporal logic. Model received from reasoning system can be verified by such specification. The formal verification enables to locate deviations from the specification. Proposed approach is useful especially in PLC rapid prototyping approach. The changes in the specification can be verified immediately, towards general specification requirements. Discrepancies between specification and the prototype are localised and can be removed before next iteration. Proposed approach improves visual analysis and fast modifications, ensuring high reliability of the constructed logic controller. The formal methods increases the reliability and quality of the parallel logic controller.