More Web Proxy on the site http://driver.im/

research-article

Open access

RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa

Authors:

Angelo Ferrando,

Viviana MascardiAuthors Info & Claims

VORTEX 2023: Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution

Pages 1 - 8

https://doi.org/10.1145/3605159.3605855

Published: 18 July 2023 Publication History

Abstract

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.

References

[1]

Davide Ancona, Angelo Ferrando, and Viviana Mascardi. 2016. Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, Erika Ábrahám, Marcello M. Bonsangue, and Einar Broch Johnsen (Eds.) (Lecture Notes in Computer Science, Vol. 9660). Springer, 47–64. https://doi.org/10.1007/978-3-319-30734-3_6

Digital Library

[2]

Davide Ancona, Angelo Ferrando, and Viviana Mascardi. 2017. Parametric Runtime Verification of Multiagent Systems. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, Kate Larson, Michael Winikoff, Sanmay Das, and Edmund H. Durfee (Eds.). ACM, Richland, SC. 1457–1459. http://dl.acm.org/citation.cfm?id=3091328

[3]

Davide Ancona, Luca Franceschini, Angelo Ferrando, and Viviana Mascardi. 2021. RML: Theory and practice of a domain specific language for runtime verification. Sci. Comput. Program., 205 (2021), 102610. https://doi.org/10.1016/j.scico.2021.102610

[4]

Najwa Abu Bakar and Ali Selamat. 2013. Runtime Verification of Multi-agent Systems Interaction Quality. In Intelligent Information and Database Systems - 5th Asian Conference, ACIIDS 2013, Kuala Lumpur, Malaysia, March 18-20, 2013, Proceedings, Part I, Ali Selamat, Ngoc Thanh Nguyen, and Habibollah Haron (Eds.) (Lecture Notes in Computer Science, Vol. 7802). Springer, Berlin, Heidelberg. 435–444. https://doi.org/10.1007/978-3-642-36546-1_45

Digital Library

[5]

Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. 2018. Introduction to Runtime Verification. In Lectures on Runtime Verification - Introductory and Advanced Topics, Ezio Bartocci and Yliès Falcone (Eds.) (Lecture Notes in Computer Science, Vol. 10457). Springer, 1–33. https://doi.org/10.1007/978-3-319-75632-5_1

[6]

Tom Bocklisch, Joey Faulkner, Nick Pawlowski, and Alan Nichol. 2017. Rasa: Open Source Language Understanding and Dialogue Management. CoRR, abs/1712.05181 (2017), arXiv:1712.05181. arxiv:1712.05181

[7]

Bhriguraj Borah, Dhrubajyoti Pathak, Priyankoo Sarmah, Bidisha Som, and Sukumar Nandi. 2018. Survey of Textbased Chatbot in Perspective of Recent Technologies. In Computational Intelligence, Communications, and Business Analytics - Second International Conference, CICBA 2018, Kalyani, India, July 27-28, 2018, Revised Selected Papers, Part II, Jyotsna Kumar Mandal, Somnath Mukhopadhyay, Paramartha Dutta, and Kousik Dasgupta (Eds.) (Communications in Computer and Information Science, Vol. 1031). Springer, 84–96. https://doi.org/10.1007/978-981-13-8581-0_7

[8]

Edmund M Clarke. 1997. Model checking. In International Conference on Foundations of Software Technology and Theoretical Computer Science. 54–56. https://doi.org/10.1007/BFb0058022

[9]

Debora C Engelmann, Angelo Ferrando, Alison R Panisson, Davide Ancona, Rafael H Bordini, and Viviana Mascardi. 2023. RV4JaCa—Towards Runtime Verification of Multi-Agent Systems and Robotic Applications. Robotics, 12, 2 (2023), 49.

[10]

Angelo Ferrando, Davide Ancona, and Viviana Mascardi. 2017. Decentralizing MAS Monitoring with DecAMon. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017. ACM, Richland, SC. 239–248. http://dl.acm.org/citation.cfm?id=3091164

Digital Library

[11]

Angelo Ferrando, Michael Winikoff, Stephen Cranefield, Frank Dignum, and Viviana Mascardi. 2019. On Enactability of Agent Interaction Protocols: Towards a Unified Approach. In Engineering Multi-Agent Systems - 7th International Workshop, EMAS 2019, Montreal, QC, Canada, May 13-14, 2019, Revised Selected Papers, Louise A. Dennis, Rafael H. Bordini, and Yves Lespérance (Eds.) (Lecture Notes in Computer Science, Vol. 12058). Springer, 43–64. https://doi.org/10.1007/978-3-030-51417-4_3

Digital Library

[12]

Andrea Gatti and Viviana Mascardi. 2022. Towards VEsNA, a Framework for Managing Virtual Environments via Natural Language Agents. In Proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy, AREA@IJCAI-ECAI 2022, Vienna, Austria, 24th July 2022, Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini, Mehrnoosh Askarpour, and Louise A. Dennis (Eds.) (EPTCS, Vol. 362). 65–80. https://doi.org/10.4204/EPTCS.362.8

[13]

2011. Robots and robotic devices – Safety requirements for industrial robots. International Organization for Standardization, Geneva, CH.

[14]

Yoo Jin Lim, Gwangui Hong, Donghwan Shin, Eunkyoung Jee, and Doo-Hwan Bae. 2016. A runtime verification framework for dynamically adaptive multi-agent systems. In 2016 International Conference on Big Data and Smart Computing, BigComp 2016, Hong Kong, China, January 18-20, 2016. IEEE Computer Society, United States. 509–512. https://doi.org/10.1109/BIGCOMP.2016.7425981

Digital Library

[15]

Donald W. Loveland. 1978. Automated theorem proving: a logical basis (Fundamental studies in computer science, Vol. 6). North-Holland. isbn:0720404991 https://www.worldcat.org/oclc/252520243

[16]

Martin Mitrevski and Martin Mitrevski. 2018. Getting started with wit. ai. Developing Conversational Interfaces for iOS: Add Responsive Voice Control to Your Apps, 143–164.

[17]

Amir Pnueli. 1977. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November. IEEE Computer Society, 46–57. https://doi.org/10.1109/SFCS.1977.32

Digital Library

[18]

Chittra Roungroongsom and Denduang Pradubsuwun. 2015. Formal Verification of Multi-agent System Based on JADE: A Semi-runtime Approach. In Recent Advances in Information and Communication Technology 2015. Springer, Germany. 297–306.

[19]

Navin Sabharwal, Amit Agrawal, Navin Sabharwal, and Amit Agrawal. 2020. Introduction to Google dialogflow. Cognitive Virtual Assistants Using Google Dialogflow: Develop Complex Cognitive Bots Using the Google Dialogflow Platform, 13–54.

[20]

Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. 2018. Formal Specification for Deep Neural Networks. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Shuvendu K. Lahiri and Chao Wang (Eds.) (Lecture Notes in Computer Science, Vol. 11138). Springer, 20–34. https://doi.org/10.1007/978-3-030-01090-4_2

[21]

Paolo Torroni, Pinar Yolum, Munindar P. Singh, Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, and Paola Mello. 2009. Modelling Interactions via Commitments and Expectations. In Handbook of Research on Multi-Agent Systems - Semantics and Dynamics of Organizational Models, Virginia Dignum (Ed.). IGI Global, Hershey, PA. 263–284. https://doi.org/10.4018/978-1-60566-256-5.ch011

Cited By

Gatti AMascardi VFerrando A(2024)RV4Chatbot: Are Chatbots Allowed to Dream of Electric Sheep?Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.411.5411(73-90)Online publication date: 21-Nov-2024
https://doi.org/10.4204/EPTCS.411.5
Gatti A(2023)Virtual Environments via Natural Language AgentsMulti-Agent Systems10.1007/978-3-031-43264-4_36(486-492)Online publication date: 7-Sep-2023
https://doi.org/10.1007/978-3-031-43264-4_36

Index Terms

RV4Rasa: A Formalism-Agnostic Runtime Verification Framework for Verifying ChatBots in Rasa

Recommendations

Model-based Runtime Verification Framework

Model-based runtime verification is an extension to the state-of-the-art runtime verification, aimed at checking at runtime the system implementation against the system model (consistency checking) and the system model against the system specification (...
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
Evaluating and Informing the Design of Chatbots
DIS '18: Proceedings of the 2018 Designing Interactive Systems Conference

Text messaging-based conversational agents (CAs), popularly called chatbots, received significant attention in the last two years. However, chatbots are still in their nascent stage: They have a low penetration rate as 84% of the Internet users have not ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

VORTEX 2023: Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution

July 2023

20 pages

ISBN:9798400702495

DOI:10.1145/3605159

General Chairs:
Davide Ancona
University of Genova, Italy
,
Giorgio Audrito
Università di Torino, Italy

Copyright © 2023 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 July 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

VORTEX '23

Sponsor:

SIGSOFT

VORTEX '23: 6th International Workshop on Verification and Monitoring at Runtime Execution

July 18, 2023

WA, Seattle, USA

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
218
Total Downloads

Downloads (Last 12 months)158
Downloads (Last 6 weeks)12

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gatti AMascardi VFerrando A(2024)RV4Chatbot: Are Chatbots Allowed to Dream of Electric Sheep?Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.411.5411(73-90)Online publication date: 21-Nov-2024
https://doi.org/10.4204/EPTCS.411.5
Gatti A(2023)Virtual Environments via Natural Language AgentsMulti-Agent Systems10.1007/978-3-031-43264-4_36(486-492)Online publication date: 7-Sep-2023
https://doi.org/10.1007/978-3-031-43264-4_36

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents