<?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-009-02-0106</article-id>
      <article-id pub-id-type="publisher-id">27930</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>F.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
          <subject>I.6.4 - Model Validation and Analysis</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Checking Object System Designs Incrementally</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Ehrich</surname>
            <given-names>Hans-Dieter</given-names>
          </name>
          <email xlink:type="simple">hd.ehrich@tu-bs.de</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Kollmann</surname>
            <given-names>Maik</given-names>
          </name>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Pinger</surname>
            <given-names>Ralf</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Technical University Braunschweig, , Germany</addr-line>
        <institution>Technical University Braunschweig</institution>
        <country>Germany</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">SIEMENS AG Transportation Systems, , Germany</addr-line>
        <institution>SIEMENS AG Transportation Systems</institution>
        <country>Germany</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Hans-Dieter Ehrich (<email xlink:type="simple">hd.ehrich@tu-bs.de</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2003</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>02</month>
        <year>2003</year>
      </pub-date>
      <volume>9</volume>
      <issue>2</issue>
      <fpage>106</fpage>
      <lpage>119</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/9E49CC32-3B36-5E63-A059-4861D90F1AD0">9E49CC32-3B36-5E63-A059-4861D90F1AD0</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996272">6996272</uri>
      <permissions>
        <copyright-statement>Hans-Dieter Ehrich, Maik Kollmann, Ralf Pinger</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>We present a method for checking global conditions for object systems in a way that avoids state space explosion. The objects referred to in a global condition are checked step by step against local conditions and communication requirements derived from the global condition. The derivation is automatic, based on information about the system structure contained in the global condition. The approach is demonstrated using model checking, but the idea works for other approaches to verification or testing as well. In our current investigation, a multi-object variant of CTL is used for expressing global conditions. The local conditions and communication requirements can be verified independently using standard model checkers. The method is illustrated by a large example (about 10 24 states) where our method shows a spectacular speedup over global model checking.</p>
      </abstract>
    </article-meta>
  </front>
</article>
