| 1. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Language Support for Verifying Reconfigurable Interacting Systems
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer (STTT). - 1433-2779 .- 1433-2787.
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 2. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Model Checking Reconfigurable Interacting Systems
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13703). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031197581
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 3. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
R-CHECK: A Model Checker for Verifying Reconfigurable MAS
- 2022
-
Ingår i: AAMAS 2022. - Virtual : AAMAS '22: Proceedings of the 21st International Conference on Autonomous Agents and Multi agent Systems.
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 4. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS, volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 5. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Incorporating Monitors in Reactive Synthesis without Paying the Price
- 2021
-
Ingår i: 19th International Symposium on Automated Technology for Verification and Analysis. - Cham : Springer.
-
Konferensbidrag (refereegranskat)abstract
- Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications 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 specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating 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 synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.
|
|
| 6. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
On the Specification and Monitoring of Timed Normative Systems
- 2021
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 7. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
- 2023
-
Ingår i: Automated Technology for Verification and Analysis (ATVA). - Germany : Springer. - 0302-9743 .- 1611-3349. - 9783031453311
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 8. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Runtime Monitoring Processes Across Blockchains
- 2021
-
Ingår i: 9th IPM International Conference on Fundamentals of Software Engineering 2021 (FSEN 2021). - Cham : Springer International Publishing.
-
Konferensbidrag (refereegranskat)abstract
- Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a setup is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated. As blockchain platforms mature and their applications increase, one can observe that instead of having one blockchain as a ‘one world computer’ multiple blockchains will co-exist while possibly interacting. Existing work for business processes within the blockchain domain have focused on single isolated blockchain implementations. In this paper, we do away with this severely limiting assumption and propose a method to monitor business processes spanning different blockchains and other off-chain servers. We apply this work to business processes expressed in BPMN along with annotations proposed for a blockchain context. We further describe how we handle blockchain interoperability by synthesizing automatically off-chain monitors, acting as notaries, that handle message passing between blockchain systems, and how we employ hash-locking for cryptographically secure token swapping.
|
|
| 9. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Runtime Verification Meets Controller Synthesis
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13701). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031198489
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 10. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Tainting in Smart Contracts: Combining Static and Runtime Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
