KOPS - Das Institutionelle Repositorium der Universität Konstanz

Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems

Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:c0554ed5dc776e1f553ea01cf77731f5

LEUE, Stefan, Wei WEI, 2011. Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems. Available under: doi: 10.1109/TSE.2011.1

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

<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/rdf/resource/123456789/401"> <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:language>eng</dc:language> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/401/2/Leue.pdf"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Leue, Stefan</dc:contributor> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/401"/> <dc:creator>Wei, Wei</dc:creator> <dc:contributor>Wei, Wei</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-10-12T09:14:21Z</dc:date> <dc:rights>deposit-license</dc:rights> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/401/2/Leue.pdf"/> <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> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:issued>2011</dcterms:issued> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Leue.pdf 85

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto