C code generation from Petri net based logic controller specification

T. Gratkowski, Grobelna I., Grobelny M., Karatkevich A.

The article focuses on programming of logic controllers. It is important that a programming code of a logic controller is executed flawlessly according to the primary specification. In the presented approach we generate C code for an AVR microcontroller from a rule-based logical model of a control process derived from a control interpreted Petri net. The same logical model is also used for formal verification of the specification by means of the model checking technique. The proposed rule-based logical model and formal rules of transformation ensure that the received implementation is consistent with the already verified specification. The approach is validated by practical experiments.