TY - JOUR
T1 - Model-based system engineering supporting production scheduling based on satisfiability modulo theory
AU - Chen, Jingqi
AU - Wang, Guoxin
AU - Lu, Jinzhi
AU - Zheng, Xiaochen
AU - Kiritsis, Dimitris
N1 - Publisher Copyright:
© 2022 Elsevier Inc.
PY - 2022/5
Y1 - 2022/5
N2 - 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.
AB - 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.
KW - KARMA language
KW - MBSE
KW - Production scheduling
KW - Property verification
KW - SMT
UR - http://www.scopus.com/inward/record.url?scp=85126060042&partnerID=8YFLogxK
U2 - 10.1016/j.jii.2022.100329
DO - 10.1016/j.jii.2022.100329
M3 - Article
AN - SCOPUS:85126060042
SN - 2452-414X
VL - 27
JO - Journal of Industrial Information Integration
JF - Journal of Industrial Information Integration
M1 - 100329
ER -