The goal of this work is to address the need for cybersecurity solutions within the world of operational technology (OT). Specifically, this work describes the development of a part of the DIANA project, a plug and play tool capable of performing automatic scanning, validation and reporting of the status of security within an OT network, in a continuous monitoring cycle. Within the context of DIANA, this thesis focuses on the development of a formal verification engine that takes as input a network description, containing information about host and network configuration, topology, and potential vulnerabilities; and generates possible attack paths and sequences of tasks to be executed in order to test the actual exploitability of the system.