<?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.3217/jucs-012-11-1551</article-id>
      <article-id pub-id-type="publisher-id">28699</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.4 - Software/Program Verification</subject>
          <subject>D.3.2 - Language Classifications</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Verifying Real-Time Properties of tccp Programs</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Alpuente</surname>
            <given-names>María</given-names>
          </name>
          <email xlink:type="simple">alpuente@dsic.upv.es</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Gallardo</surname>
            <given-names>María del Mar</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Pimentel</surname>
            <given-names>Ernesto</given-names>
          </name>
          <xref ref-type="aff" rid="A3">3</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Villanueva</surname>
            <given-names>Alicia</given-names>
          </name>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Technical University of Valencia, , Spain</addr-line>
        <institution>Technical University of Valencia</institution>
        <country>Spain</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">University of Malaga, , Spain</addr-line>
        <institution>University of Malaga</institution>
        <country>Spain</country>
      </aff>
      <aff id="A3">
        <label>3</label>
        <addr-line content-type="verbatim">Universidad de Málaga, Málaga, Spain</addr-line>
        <institution>Universidad de Málaga</institution>
        <addr-line content-type="city">Málaga</addr-line>
        <country>Spain</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: María Alpuente (<email xlink:type="simple">alpuente@dsic.upv.es</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2006</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>11</month>
        <year>2006</year>
      </pub-date>
      <volume>12</volume>
      <issue>11</issue>
      <fpage>1551</fpage>
      <lpage>1573</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/B779AF09-204C-50FC-A1CB-3B66CF22CCE9">B779AF09-204C-50FC-A1CB-3B66CF22CCE9</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6999720">6999720</uri>
      <permissions>
        <copyright-statement>María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>The size and complexity of software systems are continuously increasing, which makes them difficult and labor-intensive to develop, test and evolve. Since concurrent systems are particularly hard to verify by hand, achieving effective and automated verification tools for concurrent software has become an important topic of research. Model checking is a popular automated verification technology which allows us to determine the properties of a software system and enables more thorough and less costly testing. In this work, we improve the model-checking methodology previously developed for the timed concurrent constraint programming language tccp so that more sophisticated, real-time properties can be verified by the model-checking tools. The contributions of the paper are twofold. On the one hand, we define a timed extension of the tccp semantics which considers an explicit, discrete notion of the passing of time. On the other hand, we consistently define a real-time extension of the linear-time temporal logic that is used to specify and analyze the software properties in tccp. Both extensions fit into the tccp framework perfectly in such a way that with minor modifications any tccp model checker can be reused to analyze real-time properties. Finally, by means of an example, we illustrate the improved ability to check real-time properties.</p>
      </abstract>
    </article-meta>
  </front>
</article>
