Modeling and Analysis of an Industrial Communication Protocol in the Gamma Framework

TitleModeling and Analysis of an Industrial Communication Protocol in the Gamma Framework
Publication TypeConference Paper
Year of Publication2020
AuthorsGraics, B., and Majzik, I.
EditorRenczes, B.
Conference Name27th Minisymposium of the Department of Measurement and Information Systems
Date Published02/2020
PublisherBudapest University of Technology and Economics, Department of Measurement and Information Systems
Conference LocationBudapest, Hungary
Abstract

Communication protocols are often designed on the basis of state-based models. During protocol design, the use of formal verification is indispensable, as concurrent behavior is notorious for hidden and sophisticated bugs. This paper presents a formal verification approach to verify an industrial communication protocol using the Gamma StatechartComposition Framework. Gamma is a modeling toolset for the design and analysis of reactive systems. It supports a family of modeling languages with formal semantics for the component-based definition of state-based behavior. It also supports formal verification by automatically mapping the defined models to the input formalisms of verification backends and back-annotating the results. The verification approach is presented in the context of the Orion industrial communication protocol. The verification approach supports the introduction of channel models with different message transmission characteristics and failure modes. Different execution modes of the components are also analyzed.

Refereed DesignationRefereed
PDF: