Verifying Vaccine Supply Chain System in Indonesia Using Linear-Time Temporal Logic

摘要

We propose a formal approach to verify the safety of vaccine supply chain systems in Indonesia. The description of vaccine supply chain systems comes from PT. Bio Farma as the vaccine producer, and according to WHO regulation as well. Firstly, we describe the workflows of the system and model them using activity diagrams. Afterwards, we specify safety properties based on the WHO requirements as linear-time temporal logic formulas and translate the diagrams into temporal logic expressions in the form of NuSMV model. We verify them using NuSMV model checker to check whether the workflows conform to the requirements. In general, the result shows that the safety of the system is proven.