Design and Verification of Real-Life Processes With Application of Petri Nets
提出一种使用解释Petri网对分布式逻辑控制器进行设计与验证的方法，覆盖从规范到实现的完整流程，并通过智能家居案例验证其正确性。
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.