<?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.66455</article-id>
      <article-id pub-id-type="publisher-id">66455</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>A.1 - INTRODUCTORY AND SURVEY</subject>
          <subject>Topic D - Software</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Formal Verification of Cloud and Fog Systems:A Review and Research Challenges</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Fakhfakh</surname>
            <given-names>Fairouz</given-names>
          </name>
          <email xlink:type="simple">fairouz.fakhfakh@gmail.com</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Kallel</surname>
            <given-names>Slim</given-names>
          </name>
          <email xlink:type="simple">slim.kallel@gmail.com</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Cheikhrouhou</surname>
            <given-names>Saoussen</given-names>
          </name>
          <email xlink:type="simple">saoussen.cheikhrouhou@gmail.com</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">ReDCAD, university of sfax, Sfax, Tunisia</addr-line>
        <institution>ReDCAD, university of sfax</institution>
        <addr-line content-type="city">Sfax</addr-line>
        <country>Tunisia</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding authors: Fairouz Fakhfakh (<email xlink:type="simple">fairouz.fakhfakh@gmail.com</email>), Slim Kallel (<email xlink:type="simple">slim.kallel@gmail.com</email>), Saoussen Cheikhrouhou (<email xlink:type="simple">saoussen.cheikhrouhou@gmail.com</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2021</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>04</month>
        <year>2021</year>
      </pub-date>
      <volume>27</volume>
      <issue>4</issue>
      <fpage>341</fpage>
      <lpage>363</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/87C2264B-EF93-5E80-BDA6-D2EBF9129662">87C2264B-EF93-5E80-BDA6-D2EBF9129662</uri>
      <history>
        <date date-type="received">
          <day>13</day>
          <month>05</month>
          <year>2020</year>
        </date>
        <date date-type="accepted">
          <day>09</day>
          <month>03</month>
          <year>2021</year>
        </date>
      </history>
      <permissions>
        <copyright-statement>Fairouz Fakhfakh, Slim Kallel, Saoussen Cheikhrouhou</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>Cloud and Fog computing have been widely recognized as attractive solutions in both academic and industrial sectors. Despite their benefits, the adoption of Cloud and Fog computing still have considerable challenges to be handled due to the increase of client requirements. A crucial issue, in this context, is how to verify the correctness of Cloud and Fog systems. The use of formal methods is an efficient mean which provides a real help for the designer to evaluate the behaviour of a system and prevent errors before its implementation. In this paper, we present a systematic literature review (SLR) on the current state of the art in this field. We collect the existing studies on the use of formal methods for proving the correctness of Cloud and Fog systems. The proposed approaches are compared based on some technical properties such as the verification methods, the verification tools, the considered properties, and the application domains. In addition, future directions which need more investigations are presented. We believe that our paper will be useful for industry and academic researchers to understand the existing contributions that deal with the cor- rectness of Cloud and Fog systems. Moreover, it helps them to address several gaps in the literature.</p>
      </abstract>
    </article-meta>
  </front>
</article>
