A livelock freedom analysis for infinite state asynchronous reactive systems

Lade...
Vorschaubild
Dateien
leue_215507.pdf
leue_215507.pdfGröße: 427.79 KBDownloads: 264
Datum
2006
Autor:innen
Ştefănescu, Alin
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
BAIER, Christel, ed., Holger HERMANNS, ed.. CONCUR 2006 – Concurrency Theory. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 79-94. Lecture Notes in Computer Science. 4137. ISBN 978-3-540-37376-6. Available under: doi: 10.1007/11817949_6
Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690LEUE, Stefan, Alin ŞTEFĂNESCU, Wei WEI, 2006. A livelock freedom analysis for infinite state asynchronous reactive systems. In: BAIER, Christel, ed., Holger HERMANNS, ed.. CONCUR 2006 – Concurrency Theory. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 79-94. Lecture Notes in Computer Science. 4137. ISBN 978-3-540-37376-6. Available under: doi: 10.1007/11817949_6
BibTex
@inproceedings{Leue2006livel-21550,
  year={2006},
  doi={10.1007/11817949_6},
  title={A livelock freedom analysis for infinite state asynchronous reactive systems},
  number={4137},
  isbn={978-3-540-37376-6},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  series={Lecture Notes in Computer Science},
  booktitle={CONCUR 2006 – Concurrency Theory},
  pages={79--94},
  editor={Baier, Christel and Hermanns, Holger},
  author={Leue, Stefan and Ştefănescu, Alin 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/21550">
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21550"/>
    <dc:language>eng</dc:language>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-04T08:51:13Z</dcterms:available>
    <dcterms:title>A livelock freedom analysis for infinite state asynchronous reactive systems</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Wei, Wei</dc:contributor>
    <dcterms:issued>2006</dcterms:issued>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21550/2/leue_215507.pdf"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21550/2/leue_215507.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-04T08:51:13Z</dc:date>
    <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>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Wei, Wei</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Ştefănescu, Alin</dc:creator>
    <dcterms:bibliographicCitation>CONCUR 2006 - concurrency theory : 17th International Conference, CONCUR 2006, Bonn, Germany, August 27 - 30, 2006; proceedings / Christel Baier ... (Eds.).- Berlin [u.a.] : Springer, 2006. - S. 79-94. - (Lecture notes in computer science ; 4137). - ISBN 978-3-540-37376-6</dcterms:bibliographicCitation>
    <dc:contributor>Ştefănescu, Alin</dc:contributor>
  </rdf:Description>
</rdf:RDF>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen