Production Recipe Validation through Formalization and Digital Twin Generation
Stefano Spellini1,a, Roberta Chirico1,b, Marco Panato1,c, Michele Lora2,d and Franco Fummi1,e
1Department of Computer Science - University of Verona
aStefano.Spellini@univr.it
bRoberta.Chirico@univr.it
cMarco.Panato@univr.it
2Singapore University of Technology and Design
dMichele.Lora@univr.it
eFranco.Fummi@univr.it
ABSTRACT
The advent of Industry 4.0 is making production processes every day more complicated. As such, early process validation is becoming crucial to avoid production errors thus decreasing costs. In this paper, we present an approach to validate production recipes. Initially, the recipe is specified according to the ISA-95 standard, while the production plant is described using AutomationML. These specifications are formalized into a hierarchy of assume-guarantee contracts. Each contract specifies a set of temporal behaviors, characterizing the different machines composing the production line, their actions and interaction. Then, the formal specifications provided by the contracts are systematically synthesized to automatically generate a digital twin for the production line. Finally, the digital twin is used to evaluate, and validate, both the functional and the extrafunctional characteristics of the system.
The methodology has been applied to validate the production of a product requiring additive manufacturing, robotic assembling and transportation.
Keywords: Smart Manufacturing, Design Automation, Digital Twin, Simulation and Validation.
