<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3897/jucs.91311</article-id>
      <article-id pub-id-type="publisher-id">91311</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>D.2.1 - Requirements/Specifications</subject>
          <subject>D.2.2 - Design Tools and Techniques</subject>
          <subject>D.2.4 - Software/Program Verification</subject>
          <subject>D.2 - SOFTWARE ENGINEERING</subject>
          <subject>I.2.4 - Knowledge Representation Formalisms and Methods</subject>
          <subject>I.2 - ARTIFICIAL INTELLIGENCE</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>A Modeling Strategy for the Verification of Context-Oriented Chatbot Conversational Flows via Model Checking</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Silva</surname>
            <given-names>Geovana Ramos Sousa</given-names>
          </name>
          <email xlink:type="simple">geovannna.1998@gmail.com</email>
          <uri content-type="orcid">https://orcid.org/0000-0002-0304-0804</uri>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Rodrigues</surname>
            <given-names>Genaína Nunes</given-names>
          </name>
          <uri content-type="orcid">https://orcid.org/0000-0003-1661-8131</uri>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Canedo</surname>
            <given-names>Edna Dias</given-names>
          </name>
          <uri content-type="orcid">https://orcid.org/0000-0002-2159-339X</uri>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">University of Brasília, Brasília, Brazil</addr-line>
        <institution>University of Brasília</institution>
        <addr-line content-type="city">Brasília</addr-line>
        <country>Brazil</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Geovana Ramos Sousa Silva (<email xlink:type="simple">geovannna.1998@gmail.com</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2023</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>07</month>
        <year>2023</year>
      </pub-date>
      <volume>29</volume>
      <issue>7</issue>
      <fpage>805</fpage>
      <lpage>835</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/883A9ED5-E10A-5049-8D1C-6439C5DF291D">883A9ED5-E10A-5049-8D1C-6439C5DF291D</uri>
      <history>
        <date date-type="received">
          <day>05</day>
          <month>08</month>
          <year>2022</year>
        </date>
        <date date-type="accepted">
          <day>21</day>
          <month>02</month>
          <year>2023</year>
        </date>
      </history>
      <permissions>
        <copyright-statement>Geovana Ramos Sousa Silva, Genaína Nunes Rodrigues, Edna Dias Canedo</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="https://creativecommons.org/licenses/by-nd/4.0/" xlink:type="simple">
          <license-p>This is an open access article distributed under the terms of the Creative Commons Attribution License (CC BY-ND 4.0). This license allows reusers to copy and distribute the material in any medium or format in unadapted form only, and only so long as attribution is given to the creator. The license allows for commercial use.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>Verification of chatbot conversational flows is paramount to capturing and understanding chatbot behavior and predicting problems that would cause the entire flow to be restructured from scratch. The literature on chatbot testing is scarce, and the few works that approach this subject do not focus on verifying the communication sequences in tandem with the functional requirements of the conversational flow itself. However, covering all possible conversational flows of context-oriented chatbots through testing is not feasible in practice given the many ramifications that should be covered by test cases. Alternatively, model checking provides a model-based verification in a mathematically precise and unambiguous manner. Moreover, it can anticipate design flaws early in the software design phase that could lead to incompleteness, ambiguities, and inconsistencies. We postulate that finding design flaws in chatbot conversational flows via model checking early in the design phase may overcome quite a few verification gaps that are not feasible via current testing techniques for context-oriented chatbot conversational flows. Therefore, in this work, we propose a modeling strategy to design and verify chatbot conversational flows via the Uppaal model checking tool. Our strategy is materialized in the form of templates and a mapping of chatbot elements into Uppaal elements. To evaluate this strategy, we invited a few chatbot developers with different levels of expertise. The feedback from the participants revealed that the strategy is a great ally in the phases of conversational prototyping and design, as well as helping to refine requirements and revealing branching logic that can be reused in the implementation phase.</p>
      </abstract>
      <funding-group>
        <award-group>
          <funding-source>
            <named-content content-type="funder_name">Coordenação de Aperfeiçoamento de Pessoal de Nível Superior</named-content>
            <named-content content-type="funder_identifier">501100002322</named-content>
            <named-content content-type="funder_doi">http://doi.org/10.13039/501100002322</named-content>
          </funding-source>
        </award-group>
      </funding-group>
    </article-meta>
  </front>
</article>
