Using formal methods to model hybrid manufacturing processes

Abstract

The on-going industrial trend towards high value sustainable manufacturing has led to the emergence of hybrid manufacturing processes and resources. This new generation of processes and resources combine the capabilities of a number of older technologies on a single platform. This increase in capability, however, comes at the cost of increasing complexity. Manufacturing processes, in general, can be categorised into subtractive processes, additive processes and transformative processes. While traditional machines supported a single type of these processes (e.g. a turn-mill machine that supports multiple metal removal - subtractive - processes), the new hybrid machines combine multiple types in one device. As a result, the current process and resource models have many shortcomings in representation of hybrid processes and hybrid machines. In this research formal methods are used to construct a new type of model for hybrid manufacturing processes. Formal methods are mathematically based techniques that allow clear and non- ambiguous specification, development and, most importantly, verification of software and hardware systems. This paper utilises the ISO-standardised Z notation (named after Zermelo-Fraenkel set theory) to construct a formal model for hybrid manufacturing processes. The capabilities of the model in specification and verification of a hybrid device is then discussed through the use of a case study based on a prototype parallel kinematics hybrid manufacturing platform.