A Digital Twin (DT) is the virtual replica of an actual Cyber-Physical System
(CPS). DTs accurately replicate relevant behavioral aspects of a CPS. The
purpose of a DT is to perform computations meant to improve the performance
of the real CPS that would be resource-intensive if performed on the real
system. Examples include the real-time synthesis of adaptation policies under
uncertainty or scalability studies.
DTs are increasingly attracting attention within the manufacturing field.
Production plants are, indeed, growing complex due to the high demand for
flexible and robust solutions. Furthermore, complex manufacturing systems
are highly real-time critical since deadlocks, bottlenecks, and failures can incur
efficiency and economic losses.
In this project, we develop the formal DT of a Lego
Mindstorms production plant. The work has two main outputs: an Automata-
based model of the plant and a formal verification experimental campaign
highlighting relevant features of the system.
Detailed project description and requirements
Final Report of the project