A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:5f4f1318f5c2c0b07b81a6a98d513a26

LEUE, Stefan, Alin ŞTEFĂNESCU, Wei WEI, 2006. A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems

@techreport{Leue2006Livel-5576, series={Technical Report, Chair for Software Engineering, University of Konstanz}, title={A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems}, year={2006}, number={soft-06-02}, author={Leue, Stefan and Ştefănescu, Alin and Wei, Wei} }

<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/5576"> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5576/1/A_Livelock_Freedom_Analysis_for_Infinite_State_Asynchronous_Reactive_Systems.pdf"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Wei, Wei</dc:contributor> <dc:creator>Ştefănescu, Alin</dc:creator> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:33Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:33Z</dcterms:available> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5576/1/A_Livelock_Freedom_Analysis_for_Infinite_State_Asynchronous_Reactive_Systems.pdf"/> <dcterms:issued>2006</dcterms:issued> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> <dc:format>application/pdf</dc:format> <dcterms:title>A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems</dcterms:title> <dc:creator>Wei, Wei</dc:creator> <dc:language>eng</dc:language> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5576"/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:abstract xml:lang="eng">We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method abstracts a system into a set of simple control flow cycles labeled with their message passing effects. From these cycles, it constructs a homogeneous integer programming problem (IP) encoding a necessary condition for the existence of livelock runs. Livelock freedom is assured by the infeasibility of the generated homogeneous IP, which can be checked in polynomial time. In the case that livelock freedom cannot be proved, the method proposes a counterexample given as a set of cycles. We apply an automated cycle dependency analysis to counterexamples to check their spuriousness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive.</dcterms:abstract> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:rights>deposit-license</dc:rights> <dc:contributor>Ştefănescu, Alin</dc:contributor> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

A_Livelock_Freedom_Analysis_for_Infinite_State_Asynchronous_Reactive_Systems.pdf 98

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto