ISSTA 2023 Workshops
32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2023)
Powered by
Conference Publishing Consulting

6th International Workshop on Verification and Monitoring at Runtime Execution (VORTEX 2023), July 18, 2023, Seattle, WA, USA

VORTEX 2023 – Proceedings

Contents - Abstracts - Authors

6th Workshop on Verification and Monitoring at Runtime Execution (VORTEX 2023)

Frontmatter

Title Page


Message from the Chairs
Welcome to the 6th Workshop on Verification and Monitoring at Runtime Execution (VORTEX 2023), hosted in Seattle (WA), USA, July 18, 2023, co-located with ECOOP/ISSTA 2023.

VORTEX 2023 Organization
Committees

Full Paper

RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa
Angelo FerrandoORCID logo, Andrea Gatti ORCID logo, and Viviana MascardiORCID logo
(University of Genoa, Italy)
Chatbots are here to stay, and are going to be deployed in various application domains. Unfortunately, amongst them, there are safety-critical ones. Thus, we need a way to guarantee our chatbots will always behave as expected. In this paper, we propose RV4Rasa, a Runtime Verification framework that monitors whether a given chatbot deviates from its expected behaviour, when the latter is formalised as an interaction protocol between the end-user and the chatbot. We present RV4Rasa, its engineering, and its instantiation to monitor chatbots implemented using the Rasa framework. After presenting RV4Rasa's structure, we report experiments that we carried out in a simulated robotic scenario, where a chatbot is used to support the design of a factory workfloor.

Publisher's Version

Short Papers

On Stream Runtime Verification and Aggregate Programming
Ferruccio Damiani ORCID logo and Gianluca TortaORCID logo
(University of Turin, Italy)
Stream Runtime Verification (SRV) has been recently proposed for monitoring input streams of data while producing output streams in response. The Aggregate Programming (AP) paradigm for collection of distributed devices has been used to implement distributed runtime verification of spatial and temporal Boolean properties. In this paper we outline how distributed SRV could be implemented by AP and the new opportunities AP could bring to the field of distributed SRV.

Publisher's Version
Monitoring for Resource-Awareness
Riccardo Bianchini ORCID logo
(University of Genoa, Italy)
We show that resource-aware semantics, an execution model recently developed in the research community working on substructural type systems, can be naturally seen as a kind of monitored reduction.

Publisher's Version
Combining Static and Runtime Verification with AC and Coq
Giorgio AudritoORCID logo and Daniel Haures ORCID logo
(University of Turin, Italy)
The importance of monitoring groups of devices working together towards shared global objectives is growing, for instance when they are used for crucial purposes like search and rescue operations during emergencies. Effective approaches in this context include expressing global properties of a swarm as logical formulas in a spatial or temporal logic, which can be automatically translated into executable distributed run-time monitors. This can be accomplished leveraging frameworks such as Aggregate Computing (AC), and proving non-trivial "translation correctness" results, in which subtle bugs may easily hide if relying on hand-made proofs.
In this paper, we present an implementation of AC in Coq, which allows to automatically verify monitor correctness, further raising the security level of the monitored system. This implementation may also allow to integrate static analysis of program correctness properties with run-time monitors for properties too difficult to prove in Coq. We showcase the usefulness of our implementation by means of a paradigmatic example, proving the correctness of an AC monitor for a past-CTL formula in Coq.

Publisher's Version

proc time: 1.49