Að tryggja réttleika í dreifðum kerfum - verkefni lokið
Fréttatilkynning verkefnisstjóra
Modern software applications are architected in terms of concurrent components that execute independently and communicate via non-blocking messaging to create a dynamic, loosely-coupled software organisation known as a reactive system. This project investigates how the correctness of reactive systems can be established at runtime.
Reactive systems must:
• respond in a timely manner (be responsive),
• remain available in the face of failure (be resilient),
• grow and shrink to accommodate variable computational loads (be elastic), and
• react to inputs from users or their environment (be message-driven).
Such architectures beget many advantages (e.g. maintainability, distribution, fault isolation). At the same time, the benefits of reactive systems make the correctness in terms of their expected behaviour hard to verify statically.
We consider runtime verification (RV), which is a dynamic technique that checks the current execution of a system under scrutiny (SuS) to determine whether it satisfies or violates some correctness property. RV uses monitors—computational machines that are synthesised from formal property descriptions. Monitors are instrumented with the SuS to incrementally analyse its execution (expressed as a trace of events) and reach verdicts about its observed behaviour.
One major challenge of RV lies in choosing a monitoring approach that does not impinge on the reactive aspects of the SuS. Such a goal is met only if the monitoring system is itself reactive. This project proposes 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. We construct tools that concretise the theory and algorithms developed in this project.
We choose Erlang as our implementation language since it is specifically engineered for high-concurrency, soft real- time applications, and is one of the de facto frameworks used to build remarkably scalable and fault-tolerant distributed applications.
Information on how the results will be applied:
Our results lift previous theoretical results to accommodate scenarios where systems manipulate data. It instantiates this theory in a practical setting and bridges the gap between the theory and its application to real-world scenarios. To this end, we devise a first, decentralised outline monitoring algorithm that can be used to runtime check reactive applications. Our experiments debunk the commonly-held belief in existing literature that outline monitoring is necessarily infeasible. In fact, we argue that in cases where software components are not accessible nor amenable to modification, outline monitoring is the only viable option.
Our results also have practical uses via the tools that have been developed as part of this project. These tools have been designed for the real and practical runtime monitoring of reactive applications that run on the Erlang ecosystem.
A list of the project’s outputs:
We produced a number of publications and a suite of tools that can be used to monitor real-world, reactive applications. All of the material is openly-accessible and made available online.
Heiti verkefnis: Að
tryggja réttleika í dreifðum kerfum/Ensuring Correctness in Distributed Systems
Verkefnisstjóri:
Duncan Paul Attard, Háskólanum
í Reykjavík
Tegund styrks: Doktorsnemastyrkur
Styrktímabil: 2020-2022
Fjárhæð styrks kr. 13.250.000
Tilvísunarnúmer Rannís: 207055
