The paper proposes a novel analysis algorithm of the control part of cyber-physical systems specified by an interpreted Petri net. In particular, the three essential properties of Petri nets are studied: boundedness, safeness, and liveness. The presented idea combines linear algebra technique with reachability tree analysis. To clarify the presented concept, the method is illustrated by a real-life example of a cyber-physical system. Moreover, the experimental verification of the proposed technique was performed to examine its effectiveness and efficiency.

The paper presents a novel design methodology of cyber-physical systems supported by computer aided tools. In particular, IOPT and Hippo tools are involved in the design and analysis techniques of the system. The proposed idea combines the main advantages of both tools by offering the complex design path of the control part of the cyber-physical system, including specification, analysis and verification, decomposition, and modelling stages. Additionally, the designer is able to choose the most suitable representation of the system (graphical or formal). The presented concepts are illustrated by a case-study example.

A novel prototyping technique for concurrent control systems implemented in field programmable gate array (FPGA) devices is proposed in the paper. The method allows for dynamic modification of the implemented system. It means that the functionality of a part of the controller can be changed, while the rest of the system is still running. The approach applies to unified modeling language state machine diagrams as a specification of the system. Contrary to other methods, the presented concept requires neither major changes to the design, nor the application of external, specialized tools. The proposed idea has been experimentally verified with the use of Xilinx FPGAs.

The paper presents a method of using the UML state machine diagrams for specification of programs of logic controllers. The proposed method allows transformation from UML state machine diagram, using temporal Hierarchical Concurrent Finite State Machine (HCFSM) model, into Verilog hardware specification. The generated behavioral description in Hardware Description Language can afterwards be simulated, synthesized and implemented into e.g. FPGA device. A practical example illustrating the successive stages of the proposed method was also presented.