Please use this identifier to cite or link to this item: https://www.um.edu.mt/library/oar/handle/123456789/117964
Title: Runtime monitoring for asynchronous reactive components
Authors: Attard, Duncan Paul (2023)
Keywords: Computer software -- Verification
Formal methods (Computer science)
Algorithms
Computer programming
Aspect-oriented programming
Issue Date: 2023
Citation: Attard, D. P. (2023). Runtime monitoring for asynchronous reactive components (Doctoral dissertation).
Abstract: Modern software is built on reactive principles, where systems are responsive, resilient, elastic, and message-driven. Despite the benefits they beget, these aspects make the correctness of reactive systems in terms of their expected behaviour hard to ascertain. This thesis investigates how the correctness of reactive systems can be ascertained at runtime. It considers a lightweight monitoring technique, called runtime verification, that circumvents the issues associated with traditional pre-deployment techniques. One major challenge of runtime verification lies in choosing a monitoring approach that does not impinge on the reactive aspects of the system under scrutiny. Such a goal is met only if the monitoring system is itself reactive. We propose a novel monitoring approach grounded on this precept. It treats the system as a black box, instrumenting monitors dynamically and in asynchronous fashion, which is in tune with the requirements of reactive architectures. Our development approach is systematic, permitting us to directly map the constituent parts of our formal model to implementable modules. This gives assurances that the results obtained in the theory are preserved in the implementation. The first part of the thesis builds on established theoretical results. It lifts these results to a first-order setting to accommodate scenarios where systems manipulate data. We define an asynchronous instrumentation relation that decouples the operation of system from that of its monitors. This definition forms the basis of our decentralised outline monitoring algorithm presented in the second part of the thesis. Our algorithm employs a tracing infrastructure to collect trace events as the system executes, and uses key events as cues to instrument new monitors or terminate redundant ones dynamically. It also accounts for the interleaving of events that arises from the asynchronous execution of the system and monitors, guaranteeing that events are analysed by monitors in the correct sequence and without gaps. Part three develops a runtime veri!cation benchmarking framework that is tailored for reactive systems. The framework can generate models that faithfully capture the realistic behaviour of master-worker systems under typical load characteristics. Our tool collects di,erent performance metrics suited to reactive applications, to give a multi-faceted depiction of the overhead induced by runtime monitoring tools. Part four of this thesis embarks on an extensive evaluation of our decentralised outline monitoring algorithm using the benchmarking tool developed in part three. The algorithm is compared against our implementation of inline and centralised monitoring—two prevalent methods used in state-of-the-art runtime veri!cation tools. Apart from demonstrating that our monitoring algorithm is reactive, the experiments we conduct testify that it induces acceptable overhead that, in typical cases, is comparable to that of inlining. These results also con!rm that centralised monitoring is prone to scalability issues, poor performance, and failure, making it generally inapplicable to reactive system settings. We are unaware of other comprehensive empirical runtime veri!cation studies such as ours that compare decentralised, centralised, and inline monitoring.
Description: Ph.D.(Melit.)
URI: https://www.um.edu.mt/library/oar/handle/123456789/117964
Appears in Collections:Dissertations - FacICT - 2023
Dissertations - FacICTCS - 2023

Files in This Item:
File Description SizeFormat 
2301ICTCPS600005008983_1 (1).PDF3.49 MBAdobe PDFView/Open


Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.