University of Twente Student Theses


Formal analysis and verification of interactions in the O2N middleware framework

Bos, L.C. (2020) Formal analysis and verification of interactions in the O2N middleware framework.

[img] PDF
Abstract:The research described in this thesis aims to determine the extent to which formal methods and tools can be applied to analyze distributed systems that communicate internally using O2N, which is a middleware framework created by Thales. An analysis has been made of the characteristics of communication patterns in O2N, and it is explored which formal tools can be applied. Using one of these tools, it has been determined to what extent formal methods can be used to verify and analyze interactions between components in O2N-based systems. The main characteristic of interactions in O2N is that components are structured using a reactive architecture. Communication is often performed asynchronously, where complex message types are sent using a protocol called ’command-state’. To provide this protocol, a publish-subscribe pattern is used. An abstraction on the behaviour of components, based on their interactions, can be described using ComMA specifications. Based on these characteristics, SPIN is chosen as formal tool to perform the analysis. The ComMA specifications can be used to create the Promela models which SPIN needs. After verification, it appears that interactions in O2N can be at least verified for deadlocks, livelocks, invariants (global variable bounds), and some liveness properties. Since the limits of what SPIN can verify are being reached, it is possible to try other tools in future research to further determine the extent to which formal methods can verify and analyze O2N-based systems.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Embedded Systems MSc (60331)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page