Integer linear programming-based property checking for asynchronous reactive systems

Leue, Stefan; Wei, Wei

Integer linear programming-based property checking for asynchronous reactive systems

Dateien

Leue_243472.pdfGröße: 926.09 KBDownloads: 273

Datum

2013

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Zeitschriftenartikel

Publikationsstatus

Published

Erschienen in

IEEE Transactions on Software Engineering. 2013, 39(2), pp. 216-236. ISSN 0098-5589. Available under: doi: 10.1109/TSE.2011.1

Zusammenfassung

Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.

Fachgebiet (DDC)

004 Informatik

Zitieren

ISO 690

LEUE, Stefan, Wei WEI, 2013. Integer linear programming-based property checking for asynchronous reactive systems. In: IEEE Transactions on Software Engineering. 2013, 39(2), pp. 216-236. ISSN 0098-5589. Available under: doi: 10.1109/TSE.2011.1

BibTex

@article{Leue2013Integ-24347,
  year={2013},
  doi={10.1109/TSE.2011.1},
  title={Integer linear programming-based property checking for asynchronous reactive systems},
  number={2},
  volume={39},
  issn={0098-5589},
  journal={IEEE Transactions on Software Engineering},
  pages={216--236},
  author={Leue, Stefan and Wei, Wei}
}

RDF

<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/24347">
    <dcterms:bibliographicCitation>IEEE transactions on software engineering ; 39 (2013), 2. - S. 216-236</dcterms:bibliographicCitation>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Wei, Wei</dc:contributor>
    <dc:rights>terms-of-use</dc:rights>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/24347"/>
    <dcterms:abstract xml:lang="eng">Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.</dcterms:abstract>
    <dc:language>eng</dc:language>
    <dc:creator>Wei, Wei</dc:creator>
    <dcterms:title>Integer linear programming-based property checking for asynchronous reactive systems</dcterms:title>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/24347/1/Leue_243472.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/24347/1/Leue_243472.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-09-11T08:55:19Z</dc:date>
    <dcterms:issued>2013</dcterms:issued>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-09-11T08:55:19Z</dcterms:available>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja