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. / I detta examensarbete utforskas ett sätt att generera formella modeller av en process via inspelningar av dennes beteende. Lösningen är utvecklad från data över processens beteende, som tas upp av en digital tvilling. Det slutgiltliga målet är att med hjälp av den digitala tvillingen automatiskt generera en modell som kan användas för att verifiera säkerhet och funktioner för den riktiga processen. Lösningen blir sedan generaliserad för att i framtiden kunna bli applicerad på andra processer. Ett sätt att generera tillståndsmaskiner kommer läggas fram. Detta sätt kommer generera data för tillståndsmaskinerna genom den digitala tvillingens beteende och i framtiden planeras att användas som ett mellansteg för att generera de slutliga modellerna.  Den digitala tvillingen som används i det här projektet är implementerat av Aalto universitet, och i flera program. Den visuella delen, som även spelar in tvillingens beteende, är implementerad i Visual Components. En kontroll för den digitala tvillingen är gjord i nxtSTUDIO. Verktyget för att verifiera modellens säkerhet och funktioner är gjord i NuSMV.