This paper presents a novel design approach of a Petri-net-based cyber-physical system (CPS). The idea is oriented toward implementation in a field-programmable gate array (FPGA). The proposed technique permits error detection in the system at the early specification stage in order to reduce the time and prototyping cost of the CPS. Due to the state explosion problem, the traditional verification methods have exponential computational complexity. In contrast, we show that under certain assumptions, the proposed algorithm is able to detect possible errors in the system even in cubic O(${\left|T\right|}^2\left|P\right|$) time. Furthermore, all the required steps of the proposed design method are presented and discussed. The idea is illustrated by a real-life case study example of a traffic light crossroad. The system was modelled, analysed, implemented, and finally validated within the FPGA device (Virtex-5 family).

The paper shows the application of interpreted nets for the specification of the cyber-physical system control unit. In particular, live and safe Petri nets are taken into account in order to present the concurrency relations in the designed system. Additionally, such nets include additional input and output signals used for communication with the environment. A CPS specified by the interpreted net can be easily verified (with the application of formal methods), analyzed, decomposed and even implemented (as an integrated or distributed system). The presented idea is illustrated by a manufacturing system case study.

The paper proposes a novel design technique of cyber-physical systems (CPSs). The system is specified by a Petri net, and further modelled in a hardware description language (HDL) towards final implementation in a programmable device. Contrary to the traditional design methods, the proposed solution is highly focused on the verification aspects. The system is checked three times before the final implementation in hardware. Initially, the Petri-net based specification is formally verified by the application of the model-checking technique. Secondly, software verification of the modelled system is performed. Finally, the hardware verification of the already implemented system is executed. The proposed method is explained by an example of a direct matrix converter (MC) with transistor commutation and space vector modulation (SVM). The main benefits, as well as the limitations, of the proposed solution are discussed and analysed.

The paper proposes a novel modelling and analysis technique of the system supporting implementation of additive manufacturing (AM) technologies specified by the interpreted Petri net. Nowadays, there is a need in a manufacturing enterprise to implement the new technologies supporting the realization of production, especially in terms of the possibility of unplanned crisis events. Managers expect such models to support their decisions in order to maintain or strengthen their competitive position thanks to the investments. Therefore, this paper proposes a system supporting the decision to implement AM technology, based on the interpreted Petri net, by utilizing its main advantages: the possibility of graphical modelling, and strong mathematical support of formal verification techniques. In particular, the proposed verification algorithm allows for detection of possible unbounded places. Contrary to the most popular analysis methods (which are bounded exponential in general case), it is proved that the presented technique is bounded by a cubic polynomial with the number of Petri net nodes. Finally, the presented modelling and analysis method is illustrated by a real-life case-study example of the decision-making model to support the implementation of AM technologies. Note to Practitioners —This paper is motivated by the limited performances in the existing modelling and analysis techniques of systems that support implementation of additive manufacturing (AM) technologies. In particular, the article proposes a system supporting the decision to implement AM technology, based on the interpreted Petri net. Existing approaches have important restrictions related to the exponential computational complexity of analysis methods. Therefore, verification of the model can be a real challenge to the designer. In contradistinction, the algorithm proposed in the paper permits the examination of the system in a polynomial time. The presented modelling and analysis ideas are illustrated by a real-life example of the decision-making system that utilizes implementation of AM technology. Managers of manufacturing enterprises, thanks to the use of the proposed approach, can assess the investment in AM technology in the following three unexpected situations: 1) delays in the delivery of materials and/or semi-finished products or the inability to receive materials and/or semi-finished products; 2) high employee turnover; 3) increasing costs of energy consumption. Thus, the application of this model allows for the harmonious conduct of manufacturing activities in conditions of unexpected situations.