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.

Petri nets are a useful mathematical formalism for specification of manufacturing systems, supported by various analysis and verification methods. The progress made in automating control systems and the widespread use of Industry 4.0 pose a number of challenges to their application, starting from the education at university level and ending with modelling of real case studies. The paper aims to present and analyse the most relevant challenges and opportunities related to the use of Petri nets as a modelling technique of manufacturing systems. The review of the literature is primarily based on the years 2019–2020 to reflect the current state of the art. The newest approaches to deadlock prevention and recovering, but also other important analysis problems and difficulties in modelling real industrial processes are discussed. Trends for the future are also identified.

Human–Machine Interfaces (HMIs) in traditional automobiles are essential in connecting drivers, passengers, and vehicle systems. In automated vehicles, the HMI has become a critical component. A well-designed HMI facilitates effective human oversight, enhances situational awareness, and mitigates risks associated with system failures or unexpected scenarios. Simultaneously, it serves as a crucial safeguard against cyber threats, preventing unauthorized access and ensuring the integrity of vehicular operations in increasingly connected environments. This narrative review delves into the evolving landscape of automotive HMI design, emphasizing its role in enhancing user experience (UX) and safety. By exploring usability challenges, technological advancements, and the integration of rapidly evolving technologies such as AI (Artificial Intelligence), AR (Augmented Reality), and gesture-based controls, this study highlights how effective HMIs minimize cognitive load while maintaining functionality. Significant attention is given to the new challenges that arise from technological advancements in terms of security and safety.

In this paper, we study selected aspects of determinism in the control part of a cyber-physical system (CPS) that is specified by a Petri net-based model. In particular, the control interpreted Petri nets (CIPNs) are applied, which are an extension of the ordinary Petri nets, supplemented by signals (related to sensors and actuators) that permit communication with the environment. The notions of weak and strong determinism in a system described by a CIPN are introduced in the paper. The proposed concepts are supported by formal definitions and theorems. Moreover, a novel modelling methodology for a deterministic system specified by a CIPN is proposed. The presented solutions are illustrated by a case study example of a real-life cyber-physical system. Finally, the results of experimental verification of the proposed determinism-based techniques are demonstrated and discussed.

The paper presents the existing verification methods for control algorithms in power electronics systems, including the application of model checking techniques. In the industry, the most frequently used verification methods are simulations and experiments; however, they have to be performed manually and do not give a 100% confidence that the system will operate correctly in all situations. Here we show the recent advancements in verification and performance assessment of power electronics systems with the usage of formal methods. Symbolic model checking can be used to achieve a guarantee that the system satisfies user-defined requirements, while statistical model checking combines simulation and statistical methods to gain statistically valid results that predict the behavior with high confidence. Both methods can be applied automatically before physical realization of the power electronics systems, so that any errors, incorrect assumptions or unforeseen situations are detected as early as possible. An additional functionality of verification with the use of formal methods is to check the converter operation in terms of reliability in various system operating conditions. It is possible to verify the distribution and uniformity of occurrence in time of the number of transistor switching, transistor conduction times for various current levels, etc. The information obtained in this way can be used to optimize control algorithms in terms of reliability in power electronics. The article provides an overview of various verification methods with an emphasis on statistical model checking. The basic functionalities of the methods, their construction, and their properties are indicated.

The article focuses on some aspects regarding logic controller design. Control process is formally specified using interpreted Petri nets. It is then formally verified against behavioral properties using model checking technique and temporal logic. Formal specification can also be documented as UML activity diagram. One can then benefit from advantages of both specification techniques - Petri nets with a wide range of mathematical support and user-friendly UML activity diagrams. An interpreted Petri net can also be decomposed into state machine components (SMCs), each of them to be implemented in a separate module of FPGA device.