The student became familiar with the mathematical theory concerning Petri nets and their use in the field of industrial process modeling. He also had to learn the Codesys environment for PLC programming.
The result of the work is a demonstration model in the WoPeD environment and the corresponding PLC simulation in the CODESYS environment. I positively evaluate the systematic approach to model creation, including gradual abstraction and hierarchical division of Petri nets. The weak point of the work is the limited depth of formal verification, while the analysis is based mainly on manual work with the Petri model.
The language level is generally good, although minor grammatical and stylistic inaccuracies appear in the text. The terminology is mostly used consistently.
The practical usability of the results lies primarily in the educational and demonstration level. The proposed procedure can serve as a basis for further expansion towards formal verification of more complex industrial applications or use of automatic model checking tools.
The student worked independently and consulted on the partial procedure and problems when needed. Points proposed by supervisor: 90

The submitted thesis focuses on the use of Petri nets for modeling and analysis of a PLC-oriented control system and complements the formal model with a simple simulation in the CODESYS environment. The topic is timely and relevant to the field of industrial automation, as it connects PLC programming with formal analysis of system behavior.

The thesis has a clearly defined objective, a well-structured organization, and a solid case study of a coffee machine serving as a demonstrator of sequential and partially parallel control.

However, the thesis also contains several shortcomings. For example, in Chapter 5.6, the author describes the property of boundedness by stating that the model is bounded “as no two tokens occupy the same operational place simultaneously,” thereby confusing boundedness with the property of 1-safeness. Given that Chapter 5.6 represents the main outcome of the thesis, this error weakens the other stated claims, which are moreover not supported by a systematic formal procedure.

The thesis repeatedly uses the term formal verification and claims that Petri nets were used to analyze deadlocks, reachability, liveness, and boundedness. In reality, however, Chapters 5 through 7 show that the core of the analysis primarily relies on manual tracing of firing sequences, observation of token movements, and interpretation of several model runs. This is insufficient, as properties such as liveness or deadlock-freedom in a formal model should be supported by an appropriate analytical method.

Chapter 5 analyzes single-cycle, continuous-operation, and parallel extraction scenarios, and the conclusions present these results as supporting the usefulness of the chosen approach. At the same time, however, Chapter 6 explicitly states that the CODESYS simulation tests only single-cycle operation and that the parallel model was not implemented.

From a professional perspective, I assess the thesis as a functional demonstration study of the use of Petri nets in the design of sequential control, rather than a convincingly executed formal verification in the full sense of the term. Despite the above-mentioned shortcomings, I appreciate that the student undertook such a complex topic and recommend the thesis for defense with a grade of 80 points (B). Points proposed by reviewer: 80