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.pdfGröße: 360.42 KBDownloads: 246

Datum

2011

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Preprint

Publikationsstatus

Published

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 dependencies 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, 2011. Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems

BibTex

@unpublished{Leue2011Integ-401,
  year={2011},
  doi={10.1109/TSE.2011.1},
  title={Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems},
  author={Leue, Stefan and Wei, Wei},
  note={Zur Veröffentlichung vorgesehen in: IEEE Transactions on Software Engineering}
}

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/401">
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/401/2/Leue.pdf"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/401"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:issued>2011</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-10-12T09:14:21Z</dc:date>
    <dc:contributor>Wei, Wei</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/401/2/Leue.pdf"/>
    <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 dependencies among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real life system models.</dcterms:abstract>
    <dc:rights>terms-of-use</dc:rights>
    <dc:language>eng</dc:language>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Wei, Wei</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-10-12T09:14:21Z</dcterms:available>
    <dcterms:title>Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems</dcterms:title>
  </rdf:Description>
</rdf:RDF>

Kommentar zur Publikation

Zur Veröffentlichung vorgesehen in: IEEE Transactions on Software Engineering

Universitätsbibliographie

Ja