A Scalable Incomplete Test for Message Buffer Overflow in Promela Models

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:8df7a139c74d2f7764bb4966f614f732

LEUE, Stefan, Richard MAYR, Wei WEI, 2004. A Scalable Incomplete Test for Message Buffer Overflow in Promela Models. In: GRAF, Susanne, ed. and others. Model checking software : 11th International SPIN Workshop, Barcelona, Spain, April 1 - 3, 2004. Berlin [u.a.]:Springer, pp. 216-233. ISBN 978-3-540-21314-7

@inproceedings{Leue2004Scala-5580, title={A Scalable Incomplete Test for Message Buffer Overflow in Promela Models}, year={2004}, number={2989}, isbn={978-3-540-21314-7}, address={Berlin [u.a.]}, publisher={Springer}, series={Lecture notes in computer science}, booktitle={Model checking software : 11th International SPIN Workshop, Barcelona, Spain, April 1 - 3, 2004}, pages={216--233}, editor={Graf, Susanne}, author={Leue, Stefan and Mayr, Richard 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/5580"> <dc:rights>deposit-license</dc:rights> <dc:creator>Wei, Wei</dc:creator> <dc:contributor>Leue, Stefan</dc:contributor> <dc:creator>Leue, Stefan</dc:creator> <dc:creator>Mayr, Richard</dc:creator> <dc:contributor>Wei, Wei</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:issued>2004</dcterms:issued> <dcterms:rights rdf:resource="https://creativecommons.org/licenses/by-nc-nd/2.0/legalcode"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:bibliographicCitation>First. publ. in: Lecture notes in computer science, No. 2989 (2004) , pp. 216-233</dcterms:bibliographicCitation> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5580/1/A_Scalable_Incomplete_Test_for_Message_Buffer_Overflow_in_Promela_Models.pdf"/> <dc:format>application/pdf</dc:format> <dc:language>eng</dc:language> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:34Z</dcterms:available> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5580"/> <dcterms:abstract xml:lang="eng">In Promela, communication buffers are defined with a fixed length, and buffer overflows can be handled in two different ways: block the send statement or lose the message. Both solutions change the semantics of the system, compared to one with unbounded channels. The question arises, if such buffer overflows can ever occur in a given system and what buffer lengths are sufficient to avoid them. We describe a scalable incomplete boundedness test for the communication buffers in Promela models, which is based on overapproximation and static analysis. We first reduce Promela models to systems of communicating finite state machines (CFSMs) and then apply further abstractions that leave 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 any 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. If no such linear combination exists then the system is bounded. We discuss the complexity of this test and present experimental results using our implementation in the IBOC system. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flowgraphs derived from Promela 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. Previously, we have applied this approach to UML RT models, while in this paper we focus on the additional problems specific to Promela code: determining the potential message types of any channel, tracking potential contents of variables, channels passed as arguments to processes, channel assignments, channel arrays and parallel process creation.</dcterms:abstract> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:34Z</dc:date> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5580/1/A_Scalable_Incomplete_Test_for_Message_Buffer_Overflow_in_Promela_Models.pdf"/> <dc:contributor>Mayr, Richard</dc:contributor> <dcterms:title>A Scalable Incomplete Test for Message Buffer Overflow in Promela Models</dcterms:title> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

A_Scalable_Incomplete_Test_for_Message_Buffer_Overflow_in_Promela_Models.pdf 101

Das Dokument erscheint in:

deposit-license Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: deposit-license

KOPS Suche


Stöbern

Mein Benutzerkonto