Dependency analysis for control flow cycles in reactive communicating processes

Kurzanzeige
dc.contributor.authorLeue, Stefan
dc.contributor.authorStefanescu, Alindeu
dc.contributor.authorWei, Wei
dc.date.accessioned2011-03-23T10:15:46Zdeu
dc.date.available2011-03-23T10:15:46Zdeu
dc.date.issued2008
dc.description.abstractThe execution of a reactive system amounts to the repetitions of executions of control flow cycles in the component processes of the system. The way in which cycle executions are combined is not arbitrary since cycles may depend on or exclude one another. We believe that the information of such dependencies is important to the design, understanding, and verification of reactive systems. In this paper, we formally define the concept of a cycle dependency, and propose several static analysis methods to discover such dependencies. We have implemented several strategies for computing cycle dependencies and compared their performance with realistic models of considerable size. It is also shown how the detection of accurate dependencies is used to improve a livelock freedom analysis that we developed previously.eng
dc.description.versionpublished
dc.identifier.citationPubl. in: Model checking software: 15th International SPIN Workshop, Los Angeles, CA, USA, August 10 - 12 , 2008 ; proceedings / Klaus Havelund ... (eds.). - Berlin, Heidelberg: Springer, 2008, pp. 176-195. - (Lecture Notes in Computer Sciences ; 5156). - ISBN 978-3-540-85113-4deu
dc.identifier.doi10.1007/978-3-540-85114-1_14
dc.identifier.ppn378140825deu
dc.identifier.urihttp://kops.uni-konstanz.de/handle/123456789/3014
dc.language.isoengdeu
dc.legacy.dateIssued2010deu
dc.rightsterms-of-usedeu
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/deu
dc.subject.ddc004deu
dc.titleDependency analysis for control flow cycles in reactive communicating processeseng
dc.typeINPROCEEDINGSdeu
dspace.entity.typePublication
kops.citation.bibtex
@inproceedings{Leue2008Depen-3014,
  year={2008},
  doi={10.1007/978-3-540-85114-1_14},
  title={Dependency analysis for control flow cycles in reactive communicating processes},
  isbn={978-3-540-85113-4},
  issn={0302-9743},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  series={Lecture Notes in Computer Science},
  booktitle={Model Checking Software},
  pages={176--195},
  editor={Havelund, Klaus and Majumdar, Rupak and Palsberg, Jens},
  author={Leue, Stefan and Stefanescu, Alin and Wei, Wei}
}
kops.citation.iso690LEUE, Stefan, Alin STEFANESCU, Wei WEI, 2008. Dependency analysis for control flow cycles in reactive communicating processes. In: HAVELUND, Klaus, ed., Rupak MAJUMDAR, ed., Jens PALSBERG, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 176-195. Lecture Notes in Computer Science. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-540-85113-4. Available under: doi: 10.1007/978-3-540-85114-1_14deu
kops.citation.iso690LEUE, Stefan, Alin STEFANESCU, Wei WEI, 2008. Dependency analysis for control flow cycles in reactive communicating processes. In: HAVELUND, Klaus, ed., Rupak MAJUMDAR, ed., Jens PALSBERG, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 176-195. Lecture Notes in Computer Science. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-540-85113-4. Available under: doi: 10.1007/978-3-540-85114-1_14eng
kops.citation.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/3014">
    <dc:contributor>Stefanescu, Alin</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:title>Dependency analysis for control flow cycles in reactive communicating processes</dcterms:title>
    <dc:language>eng</dc:language>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Stefanescu, Alin</dc:creator>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:46Z</dc:date>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/3014/1/Leue_118311.pdf"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/3014/1/Leue_118311.pdf"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2008</dcterms:issued>
    <dc:contributor>Wei, Wei</dc:contributor>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/3014"/>
    <dcterms:abstract xml:lang="eng">The execution of a reactive system amounts to the repetitions of executions of control flow cycles in the component processes of the system. The way in which cycle executions are combined is not arbitrary since cycles may depend on or exclude one another. We believe that the information of such dependencies is important to the design, understanding, and verification of reactive systems. In this paper, we formally define the concept of a cycle dependency, and propose several static analysis methods to discover such dependencies. We have implemented several strategies for computing cycle dependencies and compared their performance with realistic models of considerable size. It is also shown how the detection of accurate dependencies is used to improve a livelock freedom analysis that we developed previously.</dcterms:abstract>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:rights>terms-of-use</dc:rights>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Wei, Wei</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:46Z</dcterms:available>
    <dcterms:bibliographicCitation>Publ. in: Model checking software: 15th International SPIN Workshop, Los Angeles, CA, USA, August 10 - 12 , 2008 ; proceedings / Klaus Havelund ... (eds.). - Berlin, Heidelberg: Springer, 2008, pp. 176-195. - (Lecture Notes in Computer Sciences ; 5156). - ISBN 978-3-540-85113-4</dcterms:bibliographicCitation>
  </rdf:Description>
</rdf:RDF>
kops.description.openAccessopenaccessgreen
kops.flag.knbibliographytrue
kops.identifier.nbnurn:nbn:de:bsz:352-opus-118311deu
kops.opus.id11831deu
kops.sourcefieldHAVELUND, Klaus, ed., Rupak MAJUMDAR, ed., Jens PALSBERG, ed.. <i>Model Checking Software</i>. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 176-195. Lecture Notes in Computer Science. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-540-85113-4. Available under: doi: 10.1007/978-3-540-85114-1_14deu
kops.sourcefield.plainHAVELUND, Klaus, ed., Rupak MAJUMDAR, ed., Jens PALSBERG, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 176-195. Lecture Notes in Computer Science. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-540-85113-4. Available under: doi: 10.1007/978-3-540-85114-1_14deu
kops.sourcefield.plainHAVELUND, Klaus, ed., Rupak MAJUMDAR, ed., Jens PALSBERG, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 176-195. Lecture Notes in Computer Science. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-540-85113-4. Available under: doi: 10.1007/978-3-540-85114-1_14eng
relation.isAuthorOfPublicationa0cf1380-ebf9-403b-a02e-6e97bae25ef6
relation.isAuthorOfPublication86013ecb-c2c8-4d8c-9f24-da6166bb3f33
relation.isAuthorOfPublication.latestForDiscoverya0cf1380-ebf9-403b-a02e-6e97bae25ef6
source.bibliographicInfo.fromPage176
source.bibliographicInfo.toPage195
source.contributor.editorHavelund, Klaus
source.contributor.editorMajumdar, Rupak
source.contributor.editorPalsberg, Jens
source.identifier.eissn1611-3349
source.identifier.isbn978-3-540-85113-4
source.identifier.issn0302-9743
source.publisherSpringer Berlin Heidelberg
source.publisher.locationBerlin, Heidelberg
source.relation.ispartofseriesLecture Notes in Computer Science
source.titleModel Checking Software

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
Leue_118311.pdf
Größe:
7.41 MB
Format:
Adobe Portable Document Format
Leue_118311.pdf
Leue_118311.pdfGröße: 7.41 MBDownloads: 698

Sammlungen

Informatik und Informationswissenschaft: Publikationen