The International Conference on Industrial Informatics includes several technical tracks, among which are: cyber-physical systems, internet of things and industrial agents; cloud and wireless systems for industrial applications; cognitive and computational intelligence; industrial digitalization, big data, and scheduling; and many others. Polina Ovsiannikova, a graduate of ITMO’s Computer Technologies Department and staff member of the International Laboratory “Computer Technologies”, presented a report on a new method of automated generation of formal plant models for cyber-physical systems using active learning.
A cyber-physical system is one in which a physical component is controlled by software. Among examples of a CPS is a plane engine, a milling machine or even a coffee maker. Cyber-physical systems require thorough evaluation before a final version is produced; after all, errors can cost not only money but also human lives. In most cases, a simulation model of the system is made. Simulation models reproduce a prototype’s functionality and model the processes that occur within the system. There are two main ways of evaluation: one is launching test scenarios with the simulation model in order to test the specific qualities the final version should exhibit. However, this method doesn’t guarantee that all the possible scenarios have been modeled, which is something that would take a very long time. The more formal method is formal verification.
“The most efficient method of evaluation is verification. What we do is we create a formal model of the system, equal in functionality to a simulation model. In my work, we picked a finite-state automaton as an example. Knowing that the system has input and output variables, let us suppose that each combination of output variable values is a state of the system. Changes from one state to another occur due to a combination of input signals. And so, to conduct a formal verification, we create a finite-state automaton model, specify the parameters, and upload everything into a verifier, which creates automatons based on the provided parameters, compares to the automaton that represents our system and then finds ways that contradict the input parameters (counterexamples). One advantage of this method is that we don’t need to launch each scenario manually,” explains Polina.
Despite its many advantages, formal verification (especially in a closed cycle, where both the controller and the controlled object are being verified) has one major drawback: the need for a formal model. Today, designers of cyber-physical systems rarely create formal models. It’s difficult to make formal models equivalent to simulation models and maintain them; producing them is time-consuming and demands plenty of resources and skills. Besides the fact that this approach will make the creation of formal models faster and cheaper, the existing methods also guarantee a formal model’s equivalence to a simulation one.
“A cyber-physical system consists of a controlled object (a plant) and a controller. In most cases, a formal model of the controller is created, as it is a software component and can be represented by an automaton. There are exceptions, of course. There are also methods of automated generation of controller models. But it’s a different situation with plants. Building a formal model of the plant is much more difficult since, as a physical component, it includes continuous variables like, say, the water level in the tank, the position of a part, the temperature, etc. Besides, we often only have a simulation model of the plant, which is pretty much a “black box”, as in, we can only feed it input signals and see what comes out. A formal plant model is even harder to create by hand than that of a controller, which is why I’m working on a method of generating them automatically,” says Polina.
Her proposed method is different from the existing alternatives and is based on active learning. Today, formal plant models are built using passive and active learning methods. In the case of passive learning, samples of the system’s behavior must be collected before starting to generate a model. In order to do that, one has to activate a simulation model and record the various combinations of input signals and the corresponding output signals. Recording can last a very long time, and it can be not too clear when it’s over. The data is then uploaded into a program that uses it to generate a formal model. A major drawback of this method is the possibility of errors due to the data that the model is based on. Since the endpoint for data collection is never clearly defined, the system might never achieve certain states.
The active learning method doesn’t need behavior data; only the information about the system’s input and output variables and an interface for working with the simulation model. When using this method, the model is created in the process of interacting with the original system; the information about the scenarios that have to be verified and when to finalize the model’s construction is present in the algorithm. One obstacle is that the plant may include continuous variables.
Polina Ovsiannikova’s method also uses active learning. A formal model is created as a finite-state automaton. New states are found using a breadth-first traversal algorithm. To prevent an explosion of states due to continuous variables, their value domain is sampled. For instance, if a variable assumes any value between 0 and 100, it might be sampled, i.e. its value domain is split into intervals of 0 to 20, 20 to 25 and 25 to 100. In order to take into account sampled values instead of continuous ones, two methods have been developed; both have proven functional and highly efficient in use.
However, the project does have a flaw, as of now: the finite-state automaton is massive due to the number of states and transitions, meaning that for large systems, the verification process can take too much time. The researchers are currently working on producing a model with a lesser number of transitions without loss of accuracy.
During the conference, representatives of the industry (Volkswagen, Phoenix Contact, TTTech, and others) presented their developments in the field of automated production. The event also included discussions on the use of multi-agent systems in production, and the use of digital twins and augmented reality technologies in employee training.
