Browsing by Author "Azzopardi, Shaun"

Now showing 1 - 12 of 12

AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
(International Conference on Runtime Verification, 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
Attributed Point-to-Point Communication in R-CHECK
(Lecture Notes in Computer Science (LNCS), 2024) Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir
Autonomous multi-agent, or more generally, collective adaptive systems, use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. R-CHECK is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. That is, the communication is not merely derived based on connectivity to channels but in addition based on properties of targeted receiversȦnother common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through R-CHECK’s multicast and broadcast is possible but cumbersome, inefficient, and prone to interference. Here, we extend R-CHECK with attributed point-to-point communication, which can be established based on identity or properties of participants. We also support model-checking of point-to-point by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design of models, and demonstrate their benefits by means of an illustrative case study.
Incorporating Monitors in Reactive Synthesis without Paying the Price
(19th International Symposium on Automated Technology for Verification and Analysis, 2021) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found languages that combine modelling with declarative speci - cations more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative speci cations in the presence of an existing behaviour model as a monitor, with the bene t of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeat- ing triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional syn- thesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we ap- ply it to speci cations requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametri- sation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.
Language Support for Verifying Reconfigurable Interacting Systems
(2023) Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir
Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. In this article, we provide a modeling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK. R-CHECK supports a high-level input language with matching enumerative and symbolic semantics, and provides a modelling convenience for features such as reconfiguration, coalition formation, self-organisation, etc. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.
Model Checking Reconfigurable Interacting Systems
(International Symposium on Leveraging Applications of Formal Methods, 2022) Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir
Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK (Find the associated toolkit repository here: https://github.com/dsynma/recipe.), to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, and self-organisation.
On the Specification and Monitoring of Timed Normative Systems
(2022) Azzopardi, Shaun; Pace, Gordon J.; Schapachnik, Fernando; Schneider, Gerardo
In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
(2023) Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, Gerardo
This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.
R-CHECK: A Model Checker for Verifying Reconfigurable MAS
(AAMAS 2022, 2022) Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir
Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.
Runtime Verification meets Controller Synthesis
(2022) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to interact with an environment, but the more precise the model of the environment used for synthesis, the greater the cost of synthesis. This can be avoided by using suitable abstractions of the environment, but this in turn requires appropriate techniques to mediate between controllers and the real environment. Runtime verification can help here, with monitors acting as these mediators, and even as activators or orchestrators of the desired controllers. In this paper we survey literature for combinations of monitors with controller synthesis, and consider other potential combinations as future research directions.
Runtime Verification of Kotlin Coroutines
(2022) Furian, Denis; Azzopardi, Shaun; Falcone, Yliès
Kotlin was introduced to Android as the recommended language for development. One of the unique functionalities of Kotlin is that of coroutines, which are lightweight tasks that can run concurrently inside threads. Programming using coroutines is difficult, among other things, because they can move between threads and behave unexpectedly. We introduce runtime verification in Kotlin. We provide a language to write properties and produce runtime monitors tailored to verify Kotlin coroutines. We identify, formalise and runtime verify seven properties about common runtime errors that are not easily identifiable by static analysis. To demonstrate the acceptability of the technique in real applications, we apply our framework to an in-house Android app and micro-benchmarks and measure the execution time and memory overheads.
Synchronous Agents, Verification, and Blame - A Deontic View
(2023) Kharraz, Karam; Azzopardi, Shaun; Schneider, Gerardo; Leucker, Martin
A question we can ask of multi-agent systems is whether the agents’ collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, or a specification is violated, a pertinent question is whether any agent is to blame. This paper considers a two-agent synchronous setting and a formal language to specify when agents’ collaboration is required. We take a deontic approach and use obligations, permissions, and prohibitions to capture notions of non-interference between agents. We also handle reparations, allowing violations to be corrected or compensated. We give trace semantics to our logic, and use it to define blame assignment for violations. We give an automaton construction for the logic, which we use as the base for model checking and blame analysis. We also further provide quantitative semantics that is able to compare different interactions in terms of the required reparations.
Tainting in Smart Contracts: Combining Static and Runtime Verification
(Lecture Notes in Computer Science book series (LNCS,volume 13498), 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, for instance with off-chain oracles, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn, would depend on which parties or what information contributed to them. In this paper, we develop and present dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance for ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.