Modelling a Distributed Data Acquisition System

Show full item record



Permalink

http://urn.fi/URN:NBN:fi:hulib-202107263429
Title: Modelling a Distributed Data Acquisition System
Author: Lång, John
Contributor: University of Helsinki, Faculty of Science
Publisher: Helsingin yliopisto
Date: 2021
Language: eng
URI: http://urn.fi/URN:NBN:fi:hulib-202107263429
http://hdl.handle.net/10138/332592
Thesis level: master's thesis
Degree program: Tietojenkäsittelytieteen maisteriohjelma
Master's Programme in Computer Science
Magisterprogrammet i datavetenskap
Specialisation: Algoritmit
Algorithms
Algoritmer
Abstract: This thesis discusses the formal modelling and verification of certain non-real-time aspects of correctness of a mission-critical distributed software system known as the ALICE Data Point Service (ADAPOS). The domain of this distributed system is data acquisition from a particle detector control system in experimental high energy particle physics research. ADAPOS is part of the upgrade effort of A Large Ion Collider Experiment (ALICE) at the European Organisation for Nuclear Research (CERN), near Geneva in France/Switzerland, for the third run of the Large Hadron Collider (LHC). ADAPOS is based on the publicly available ALICE Data Point Processing (ADAPRO) C++14 framework and works within the free and open source GNU/Linux ecosystem. The model checker Spin was chosen for modelling and verifying ADAPOS. The model focuses on the general specification of ADAPOS. It includes ADAPOS processes, a load generator process, and rudimentary interpretations for the network protocols used between the processes. For experimenting with different interpretations of the underlying network protocols and also for coping with the state space explosion problem, eight variants of the model were developed and studied. Nine Linear Temporal Logic (LTL) properties were defined for all those variants. Large numbers of states were covered during model checking even though the model turned out to have a reachable state space too large to fully exhaust. No counter-examples were found to safety properties. A significant amount of evidence hinting that ADAPOS seems to be safe, was obtained. Liveness properties and implementation-level verification among other possible research directions remain open.
Subject: distributed systems
control systems
data acquisition
formal verification
model checking
case study


Files in this item

Total number of downloads: Loading...

Files Size Format View
Laang_John_Mode ... cquisition_System_2021.pdf 768.8Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record