Towards finding the appropriate level of abstraction to model and verify automated production systems in discrete event simulation

Developing complex automated production systems (aPS) by integrating different engineering disciplines, e.g. electrical/electronic, mechanical or software engineering, is a rising challenge for plant manufacturing. Hence, different approaches for virtual commissioning and validating aPS have been developed in the past. Among other approaches, concepts for model verification based on discrete event systems (DES) and formal verification techniques, e.g. model checking, of aPS are commonly investigated. This paper intends to analyze and assess the appropriate level of abstraction for modeling aPS containing complex mechatronic phenomena in DES required to enable formal verification of an aPS' characteristics. For example, the modeling of the gear backlash between a handling component and its electrical drive as a possible consequence of worn gear/spindle inside a simple lab-size aPS is considered.