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.
|
PDF
2MB |
| 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: | https://purl.utwente.nl/essays/82812 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page