Model-based system engineering supporting production scheduling based on satisfiability modulo theory

Production scheduling enables a production system to allocate resources for the efficient and low-cost production. However, pure mathematical methods are typically utilized for production scheduling, which are not understandable and practical for different domain engineers. Moreover, heterogeneous information during production scheduling may result in communication ambiguity or an information delay. Furthermore, the interaction and reuse of production data is limited, owing to the lack of a unified expression of the production information. To overcome these challenges, a model-based systems engineering (MBSE) approach based on the satisfiability modulo theory (SMT) is proposed to support production scheduling. A multiple architectural view modeling language, KARMA, is used as the basis to construct production scheduling elements and formalize the production scheduling processes using architecture models. Such graphical models are used to improve the understanding and communication among engineers in different domains. Then, property verification based on the MBSE and SMT is applied to solve the model constraints and select optimal schemes for the production scheduling. A case study of a package production line is proposed to evaluate our approach. Its scheduling goal is to maintain high production efficiency, decrease the working time and the cost of workers when increasing working distances during the COVID-19 pandemic. From the case study, we observed that KARMA language enables a description of modeling production scheduling and the optimization of scheduling schemes in a unified manner. Using the SMT solver, the constraints on scheduling corresponding to the sudden decrease in workers are evaluated to exclude inappropriate schemes and generate the optimal one.