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

CímModeling and Analysis of an Industrial Communication Protocol in the Gamma Framework
Közlemény típusaConference Paper
Kiadás éve2020
SzerzőkGraics, B., and Majzik, I.
SzerkesztőRenczes, B.
Konferencia neve27th Minisymposium of the Department of Measurement and Information Systems
Kiadás dátuma02/2020
KiadóBudapest University of Technology and Economics, Department of Measurement and Information Systems
Konferencia helyszíneBudapest, Hungary
Összefoglalás

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: