Plant Model Generator from Digital Twin for Purpose of Formal Verification

Abstract: This master thesis will cover a way to automatically generate a formal model for plant verification from plant traces. The solution will be developed from trace data, stemming from a model of a digital twin of a physical plant. The final goal is to automatically generate a formal model of the plant that can be used for model checking for verifying the safety and functional properties of the actual plant. The solution for this specific setup will be generalized and a general approach for other systems will be discussed. Furthermore, state machine generation will be introduced. This includes generating state machine data from traces, and in the future is planned be used as an intermediate step between the trace data and model generation. The digital twin solution used in this project is a joint setup in Visual Components and nxtSTUDIO. The symbolic model checker NuSMV is utilized in order to verify the functional properties of the plant.