Design and Verification of Real-Life Processes With Application of Petri Nets
Iwona Grobelna, Remigiusz Wiśniewski, Michał Grobelny, Monika Wisniewska · IEEE Transactions on Systems Man and Cybernetics Systems · 2016
This paper focuses on the design and verification methods of distributed logic controllers supervising real-life processes. Such systems have to be designed very carefully and precisely in order to operate flawlessly and to meet user needs. We propose to use interpreted Petri nets as modeling formalism. A new design flow of distributed logic controllers is introduced. The methodology covers the development process from the specification stage to the final implementation of the controller in the distributed devices. In the proposed solution, the system is decomposed into separate modules that form a distributed system. Furthermore, the specification (before and after the decomposition process) is formally verified with the application of the model checking technique against predefined behavioral requirements. Finally, the system is implemented in real devices. The usage of formal methods and double model checking ensure the correct functionality of the designed distributed logic controller. The theoretical approach is supplemented by the practical experiments. Furthermore, the proposed idea is illustrated by an example of a smart home system.