Informatics in Education

Background: Petri nets are a formal specification technique for modelling of control processes and modern flexible manufacturing systems. Interpreted Petri nets take into account input and output signals, allowing to apply them in any control system or even in control part of a cyber-physical system. Due to the fact that Petri nets are not used in the industrial practice, the students sometimes lack motivation to learn them. Contributions: In the paper we propose how to help students learn interpreted Petri nets with Minecraft (as a game-based learning). We show how interpreted Petri nets can be modelled in Minecraft and how they communicate with the surrounding environment via input and output signals to visualize control processes. The proposed approach has been validated experimentally among university students. Hypotheses: (1) Creating interpreted Petri net models with Minecraft helps to understand the basic principles; (2) Minecraft makes the course more attractive. Methodology: Students were divided into an experimental group (with game-based learning) and a control group (with traditional learning). The experimental group filled in a knowledge test twice (on the entry and on the exit) and a questionnaire. The control group filled in the same knowledge test at the end of the course. Findings: The observations confirm that the Minecraft-based teaching of interpreted Petri nets allows to gain better results in final tests, making at the same time the course more attractive and enjoyable.

Control systems are becoming ever more commonly used in everyday life. This is true both in industry and in the domestic domain, in the form of e.g., smart home systems. The quality of such systems can be increased by using formal verification methods, such as the model checking technique, to make sure that the designed system fulfills all user requirements. The requirements are usually written as temporal logic formulas. However, the technical skills of future users or the mathematical background knowledge of the developers are not always sufficient to support the essential stage of verification. In the paper we propose to use the Scratch-based user-friendly approach to define our own scenarios for a control system, in order to avoid focusing on the mathematical notation of temporal requirements. The specified properties can then be transformed into temporal logic formulas and used directly in the model checking process. Hence, the verification phase is simplified and more team members can participate in the engineering of requirements. An empirical study with students has shown that the proposed approach can be used in practice.