The growing global population and the increasing scarcity of arable land highlight the urgent need for reliable and efficient food production systems. With their controlled environments, vertical farms (VFs) offer a promising solution for sustainable food security. Nevertheless, their high energy demands call for innovative approaches to optimize energy consumption while maintaining optimal growing conditions. This paper introduces a novel control-oriented model for VFs, capturing the interactions between crop growth conditions and energy consumption. To address the high energy demand of VFs, the model is integrated into a dynamic energy market characterized by time-varying energy prices and a demand response scheme, which includes a discrete reward to encourage flexible energy consumption. Then, centralized and decentralized receding horizon control approaches are proposed to minimize the energy cost of the VF while ensuring optimal crop growth. Experimental evaluations on real systems of varying scales demonstrate the effectiveness of the proposed approaches in reducing costs and ensuring sustainable agricultural practices.

Modernization of currently operational nuclear power plants is becoming increasingly important to maintain their performance and safety. Ensuring the safety of newer Instrumentation and Control (I&C) systems used in modernization efforts requires hazard analysis techniques suitable for the analysis of complex and software-heavy systems. System-Theoretic Process Analysis (STPA) has proven to be a suitable hazard analysis method for these complex I&C systems, however, its practical use is still often limited by its labor-intensive and time-consuming nature, partially due to the limitations of the tools used to perform the analysis: common Office tools such as Microsoft Excel or Visio. Conducting an STPA analysis could be simpler and more attractive with software tools specific to the method. This work introduces the requirements for these software tools and lays the foundation for further work, in which software tools will be evaluated against these requirements.

This work develops a concept of a natural language co-pilot for the creation of IEC 61499 applications to accelerate initial testing and development. The co-pilot addresses the challenge of generating the correct function blocks that can be opened in popular IEC 61499 IDEs. In our case study, we focus on the generation of the centralised controller that operates particular equipment to perform a defined process. In addition, we have developed a scheme for how the co-pilot will be integrated into the FBME IDE as an AI assistant in the next steps. In the discussion, we provide valuable information for future co-pilot developers on the possible problems they might face in this area and how to overcome them.

This paper proposes a framework designed to optimise energy consumption in vertical farming. It aims to maximise cost efficiency by balancing between minimising system operations during the electricity price peaks and the ability to trade capacity on the FCR market while also fulfilling constraints on the internal growing process. We consider that the vertical farming system has distributed control with a series of actuators controlled by various spatially distributed PLCs that we refer to as agents, to underline their independence. The paper conducts two experiments for a lO-agent system with a Pareto controller and a lOO-agent system with a Lagrangian approach and shows the balance between more cost-efficient momentary energy consumption control.

We present an approach for suggesting possible fixes to an overall I&C nuclear architecture during its design phase. Despite the I&C architecture, in our case, being represented with an ontology, we do not aim to change the properties of an ontology per se. Instead, we focus on the subset of ABox triples that do not contain terminological elements in either subject, predicate, or object parts. Such a subset we call the design artifacts. When the ontology is filled with the design artifacts, the analyst runs the check of non-functional requirements using SPARQL queries. The requirements associated with the queries that returned results do not hold. The goal of the current work is to provide support for the next stage when the analyst has to change the design artifacts so that the queries no longer return results. Our method is based on representing the results of queries as graphs, intersecting them, and finding the minimal changes that prevent the results from being mapped on their (or other) queries.

IEC 61499 is an emerging standard for distributed automation which requires well-defined design practises to improve development efficiency. In this paper, we extend the one-line engineering design pattern and provide step-by-step guidelines on its implementation keeping in mind key features of Industry 4.0. The one-line design pattern simplifies the modification of the application structure and the addition of new components to the system without disrupting the existing control application. It also enables easy fault identification and debugging of the system. The design pattern was developed and validated in three different use cases that demonstrated the applicability of the pattern.

We present an approach for suggesting possible repairs for the control logic of I&C systems implemented in the form of function block diagrams (FBDs) during the design phase. Each FBD has a set of functional requirements formulated using linear temporal logic (LTL). To ensure the correctness of the implementation, an FBD is translated into SMV, the language of the NuSMV model checker, which verifies the model against its properties. If a property does not hold, NuSMV generates a counterexample. In previous works, we developed methods on visual counterexample explanation using both, the failing LTL formula and the FBD itself. The current work continues in this direction and utilizes the results of the counterexample explanation to suggest fixes to the FBD considering the failed properties and the whole set of requirements. We propose three strategies for fixes generation and experiment on the examples of the logic from the nuclear domain.

Distributed automation systems design is getting increasingly popular as the systems become more complex and modular. The IEC 61499 automation architecture is seen as the main enabler of component software design for distributed automation systems. It requires novel approaches to integrated development environments (IDE) supporting the engineering of such component software systems. One important part of automation systems engineering is their verification and validation. The efficacy of verification is largely dependent on how seamlessly this process is integrated with the traditional development tools, such as editors, compilers and debuggers. This work presents a start of such a development, that automatizes the model checking process for IEC 61499 systems and provides a visual explanation of its results in the graphical development environment FBME.

Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.

Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present OERITTE, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, OERITTE serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.

As the world becomes more and more automated, the degree of cyber-physical systems involvement cannot be overestimated. A large part of them are safety-critical, thus, it is especially important to ensure their correctness before start of operation or reconfiguration. For this purpose the model checking approach should be used since it allows rigorously proving system correctness by checking all possible states. To ensure the compliance of controller-plant properties with system requirements, the closed-loop verification approach should be chosen, which requires not only a formal model of the controller, but also a formal model of the plant. In this paper we propose an approach for constructing formal models of context-free deterministic plants automatically using active learning algorithms. The case study shows its successful application to plant model generation for the elevator cyber-physical system.

Cyber-physical systems are spread among multiple domains of human activity. Their behavior should be strictly validated as most of them are critical. One perspective direction of ensuring system correctness is verification using model checking. A new method for closed-loop model checking of cyber-physical systems has recently been introduced that involves automatic formal plant model synthesis followed by temporal properties verification. The formal model is inferred based on traces gathered from the simulation model. Then, verification of temporal properties for the whole closed-loop system can be performed using the NuSMV tool. The main purpose of this paper is to investigate the applicability of the aforementioned method by performing a case study on the example of a compensating group drive simulation model provided by our industrial partners.