Formal correctness of supply chain design

Many companies use supply chain models for designing the flow of goods and services from their suppliers all the way up to the final customers. Over the past 15 years, the Supply Chain Operations Reference Model (SCOR) has become a widespread modeling technique for designing such supply chains and sharing design information with supply chain stakeholders. However, neither the syntax nor the semantics of SCOR are well defined. This limitation has important consequences for its usage: Supply chain models may be ambiguous and their correctness cannot be verified. We address this problem by mapping SCOR supply chains onto graphs and formalize the semantics of SCOR. The mapping is driven by constructs from the supply chain management literature. The proposed artifact is a supply chain grammar, which we apply to a set of SCOR models taken from industry sources. We show the grammar's usefulness by verifying the correctness of these models using analytical techniques.