Download PDFOpen PDF in browserVerifying UML-RT Model of a Conveyor Belt System with nuXmv Model CheckerEasyChair Preprint 49436 pages•Date: January 30, 2021AbstractConveyor 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
|