VORTEX '23: "Combining Static and Runtime ..."
Combining Static and Runtime Verification with AC and Coq
Giorgio Audrito and Daniel Haures
(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.
@InProceedings{VORTEX23p17,
author = {Giorgio Audrito and Daniel Haures},
title = {Combining Static and Runtime Verification with AC and Coq},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {17--20},
doi = {10.1145/3605159.3605857},
year = {2023},
}
Publisher's Version
VORTEX '23: "Monitoring for Resource-Awareness ..."
Monitoring for Resource-Awareness
Riccardo Bianchini
(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.
@InProceedings{VORTEX23p13,
author = {Riccardo Bianchini},
title = {Monitoring for Resource-Awareness},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {13--16},
doi = {10.1145/3605159.3605856},
year = {2023},
}
Publisher's Version
VORTEX '23: "On Stream Runtime Verification ..."
On Stream Runtime Verification and Aggregate Programming
Ferruccio Damiani and Gianluca Torta
(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.
@InProceedings{VORTEX23p9,
author = {Ferruccio Damiani and Gianluca Torta},
title = {On Stream Runtime Verification and Aggregate Programming},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {9--12},
doi = {10.1145/3605159.3605854},
year = {2023},
}
Publisher's Version
VORTEX '23: "RV4Rasa: A Formalism-Agnostic ..."
RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa
Angelo Ferrando, Andrea Gatti, and Viviana Mascardi
(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.
@InProceedings{VORTEX23p1,
author = {Angelo Ferrando and Andrea Gatti and Viviana Mascardi},
title = {RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3605159.3605855},
year = {2023},
}
Publisher's Version
VORTEX '23: "RV4Rasa: A Formalism-Agnostic ..."
RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa
Angelo Ferrando, Andrea Gatti, and Viviana Mascardi
(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.
@InProceedings{VORTEX23p1,
author = {Angelo Ferrando and Andrea Gatti and Viviana Mascardi},
title = {RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3605159.3605855},
year = {2023},
}
Publisher's Version
VORTEX '23: "Combining Static and Runtime ..."
Combining Static and Runtime Verification with AC and Coq
Giorgio Audrito and Daniel Haures
(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.
@InProceedings{VORTEX23p17,
author = {Giorgio Audrito and Daniel Haures},
title = {Combining Static and Runtime Verification with AC and Coq},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {17--20},
doi = {10.1145/3605159.3605857},
year = {2023},
}
Publisher's Version
VORTEX '23: "RV4Rasa: A Formalism-Agnostic ..."
RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa
Angelo Ferrando, Andrea Gatti, and Viviana Mascardi
(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.
@InProceedings{VORTEX23p1,
author = {Angelo Ferrando and Andrea Gatti and Viviana Mascardi},
title = {RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3605159.3605855},
year = {2023},
}
Publisher's Version
VORTEX '23: "On Stream Runtime Verification ..."
On Stream Runtime Verification and Aggregate Programming
Ferruccio Damiani and Gianluca Torta
(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.
@InProceedings{VORTEX23p9,
author = {Ferruccio Damiani and Gianluca Torta},
title = {On Stream Runtime Verification and Aggregate Programming},
booktitle = {Proc.\ VORTEX},
publisher = {ACM},
pages = {9--12},
doi = {10.1145/3605159.3605854},
year = {2023},
}
Publisher's Version