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.

This paper shows a novel prototyping technique for concurrent control systems described by interpreted Petri nets. The technique is based on the decomposition of an interpreted Petri net into concurrent sequential automata. In general, minimum decomposition requires runtime that is exponential in the number of Petri net places. We show that in many cases, including the real-life ones, the minimum decomposition problem can be solved in polynomial time. The proposed method allows implementing a concurrent control system using minimal number of sequential components, which requires polynomial time and can be applied to most of the considered cases. The presented concept is illustrated by a real-life industrial example of a beverage production and distribution machine implemented in a field programmable gate array.

The Internet of Medical Things (IoMT) global market has grown and developed significantly in recent years, and the number of IoMT devices is increasing every year. IoMT systems are now very popular and have become part of our everyday life. However, such systems should be properly protected to preventing unauthorized access to the devices. One of the most popular security methods that additionally relies on real-time communication is Blockchain. Moreover, such a technique can be supported by the Trusted Third Party (TTP), which guarantees data immutability and transparency. The research and industrial community has predicted the proliferation of Blockchain-based IoMT (BIoMT), for providing security, privacy, and effective insurance processing. A connected environment comprises some of the unique features of the IoMT in the form of sensors and devices that capture and measure, recognize and classify, assess risk, notify, make conclusions, and take action. Distributed communication is also unique due to the combination of the fact that the Blockchain cannot be tampered with and the Peer-to-Peer (P2P) technique, especially compared to the traditional cloud-based techniques where the reliance of IoMT systems on the centralized cloud makes it somewhat vulnerable. This paper proposes a Blockchain-based technique oriented on IoMT applications with a focus on maintaining Confidentiality, Integrity, and Availability (the CIA triad) of data communication in the system. The proposed solution is oriented toward trusted and secure real-time communication. The presented method is illustrated by an example of a cloud-based hospital application. Finally, the security aspects of the proposed approach are studied and analyzed in detail.

This paper proposes a novel design concept of concurrent control systems specified by interpreted Petri nets and implemented in Xilinx FPGA devices. The technique is oriented on further dynamic partial reconfiguration of the system. An adequate splitting algorithm of the system into the dynamic (reconfigurable) and static (non-reconfigurable) partitions is proposed. The main advantage of the presented idea is the possibility of the dynamic reconfiguration of the already implemented system. It means that the functionality of the selected component (module) of the controller can be changed, while the rest of the system is still running. The presented technique is illustrated by a real-life case-study example, and it has been verified experimentally with the application of Xilinx FPGA device.