Verifying UML-RT Model of a Conveyor Belt System with nuXmv Model Checker

EasyChair Preprint no. 4943

Abstract

Conveyor belt system is a convenient and reliable system used in automated distribution of goods and merchandise. The effectiveness of merging items from multiple induction lines onto one main line is one of the important aspects in implementing such a labour-saving system. One way of ensuring correctness and reliability for such a system is by introducing model-checking at design level. In this paper, a simple conveyor belt system is first modelled using Papyrus-RT, which is an implementation of the UML-RT modelling language. Then, based on a set of translation rules, this model is mechanically translated into the nuXmv symbolic model checker for property verification. Counter examples are presented in case of incorrect properties or failures inside the model, along with a log trace comparison indicating time-dependent inconsistencies between nuXmv and Papyrus-RT models.

Keyphrases: Conveyor belt system, model translation, nuXmv, Papyrus-RT, symbolic model checking, UML-RT

@Booklet{EasyChair:4943,
  author = {Duy Hieu Vo and Minh Gia Huy Cao and Nhat Nam Pham and Tong Ngoc Dang and Sneha Sahu and Ruth Schorr},
  title = {Verifying UML-RT Model of a Conveyor Belt System with nuXmv Model Checker},
  howpublished = {EasyChair Preprint no. 4943},

  year = {EasyChair, 2021}}