Publikation:

A Scalable Incomplete Test for the Boundedness of UML RT Models

Vorschaubild

Dateien

A_Scalable_Incomplete_Test_for_the_Boundedness_of_UML_RT_Models.pdf
A_Scalable_Incomplete_Test_for_the_Boundedness_of_UML_RT_Models.pdfGröße: 234.05 KBDownloads: 341

Datum

2004

Autor:innen

Mayr, Richard

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-57783
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-540-24730-2_26
ArXiv-ID

Internationale Patentnummer

Link zur Lizenz
Attribution-NonCommercial-NoDerivs 2.0 Generic

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

JENSEN, Kurt, ed., Andreas PODELSKI, ed.. Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 327-341. Lecture Notes in Computer Science. 2988. ISBN 978-3-540-21299-7. Available under: doi: 10.1007/978-3-540-24730-2_26

Zusammenfassung

We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We reduce UML RT models to systems of communicating finite state machines (CFSMs). We propose a series of further abstractions that leaves us with a system of linear inequalities. Those represent the message sending and receiving effect that the control flow cycles of every process have on the overall message buffer. The test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. We discuss the complexity of this test and present experimental results using the IBOC system that we are implementing. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flow graphs that are derived from UML RT models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models.We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. While we focus on the analysis of UML RT models, the analysis
can directly be applied to any type of CFSM models.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690LEUE, Stefan, Richard MAYR, Wei WEI, 2004. A Scalable Incomplete Test for the Boundedness of UML RT Models. In: JENSEN, Kurt, ed., Andreas PODELSKI, ed.. Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 327-341. Lecture Notes in Computer Science. 2988. ISBN 978-3-540-21299-7. Available under: doi: 10.1007/978-3-540-24730-2_26
BibTex
@inproceedings{Leue2004Scala-5567,
  year={2004},
  doi={10.1007/978-3-540-24730-2_26},
  title={A Scalable Incomplete Test for the Boundedness of UML RT Models},
  number={2988},
  isbn={978-3-540-21299-7},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  series={Lecture Notes in Computer Science},
  booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
  pages={327--341},
  editor={Jensen, Kurt and Podelski, Andreas},
  author={Leue, Stefan and Mayr, Richard 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/5567">
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5567/1/A_Scalable_Incomplete_Test_for_the_Boundedness_of_UML_RT_Models.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:29Z</dc:date>
    <dcterms:abstract xml:lang="eng">We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We reduce UML RT models to systems of communicating finite state machines (CFSMs). We propose a series of further abstractions that leaves us with a system of linear inequalities. Those represent the message sending and receiving effect that the control flow cycles of every process have on the overall message buffer. The test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. We discuss the complexity of this test and present experimental results using the IBOC system that we are implementing. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flow graphs that are derived from UML RT models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models.We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. While we focus on the analysis of UML RT models, the analysis&lt;br /&gt;can directly be applied to any type of CFSM models.</dcterms:abstract>
    <dc:creator>Wei, Wei</dc:creator>
    <dc:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights>
    <dcterms:title>A Scalable Incomplete Test for the Boundedness of UML RT Models</dcterms:title>
    <dcterms:bibliographicCitation>First publ. in: Lecture notes in computer science, No. 2988 (2004), pp. 327-341</dcterms:bibliographicCitation>
    <dc:format>application/pdf</dc:format>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Mayr, Richard</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:29Z</dcterms:available>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5567"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Wei, Wei</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5567/1/A_Scalable_Incomplete_Test_for_the_Boundedness_of_UML_RT_Models.pdf"/>
    <dc:language>eng</dc:language>
    <dcterms:issued>2004</dcterms:issued>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Mayr, Richard</dc:creator>
    <dc:contributor>Leue, Stefan</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