返回
Model-based system engineering supporting production scheduling based on satisfiability modulo theory
DOI:10.1016/j.jii.2022.100329.png)
摘要
En 中文
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.
Keyword:
Production scheduling
MBSE
SMT
Property verification
KARMA language
AI总结
对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
期刊
IF:
11.6
论文数:
906
被引数:
4.4K

