Download PDFOpen PDF in browser

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

EasyChair Preprint 4943

6 pagesDate: January 30, 2021

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, Papyrus-RT, UML-RT, model translation, nuXmv, symbolic model checking

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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 4943},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser