Implementing and Verifying MSC Specifications Using Promela/XSpin

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:fd0d5740d427dae150fc71a20db23ea2

LEUE, Stefan, Peter B. LADKIN, 1997. Implementing and Verifying MSC Specifications Using Promela/XSpin. DIMACS, 5. Aug 1996. In: GRÉGOIRE, Jean-Charles, ed. and others. The SPIN verification system : proceedings of a DIMACS workshop, August 5, 1996, the Second Workshop on the SPIN Verification System. DIMACS, 5. Aug 1996. Providence:American Mathematical Society

@inproceedings{Leue1997Imple-5423, title={Implementing and Verifying MSC Specifications Using Promela/XSpin}, year={1997}, address={Providence}, publisher={American Mathematical Society}, booktitle={The SPIN verification system : proceedings of a DIMACS workshop, August 5, 1996, the Second Workshop on the SPIN Verification System}, editor={Grégoire, Jean-Charles}, author={Leue, Stefan and Ladkin, Peter B.} }

<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/5423"> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5423/1/Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf"/> <dc:language>eng</dc:language> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:15Z</dcterms:available> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5423/1/Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf"/> <dc:contributor>Ladkin, Peter B.</dc:contributor> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:abstract xml:lang="eng">We discuss a translation of Message Sequence Charts (MSCs) into the language PROMELA (we call this translation an 'implementation') that is consistent with the formal semantics we have previously defined for Message Flow Graphs and Message Sequence Charts, which handled the syntactic features with mathematical import from ITU-T recommendation Z.120. We report on experiments executing the PROMELA code using XSPIN simulator and validator. In previous work we found that potential process divergence and non-local choice situations impose problems on implementations of MSCs, and we discuss how these impact our PROMELA translation and suggest solutions. Finally, we show how to model-check liveness requirements imposed on MSC specifications. We used the PROMELA models obtained from our implementation , describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSPIN as a model checker for these properties.</dcterms:abstract> <dc:format>application/pdf</dc:format> <dc:rights>deposit-license</dc:rights> <dc:creator>Ladkin, Peter B.</dc:creator> <dcterms:bibliographicCitation>First publ. in: The SPIN verification system : proceedings of a DIMACS workshop, August 5, 1996, the Second Workshop on the SPIN Verification System / Eds:Jean-Charles Grégoire ... Providence : American Mathematical Society, 1997</dcterms:bibliographicCitation> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5423"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:rights rdf:resource="https://creativecommons.org/licenses/by-nc-nd/2.0/legalcode"/> <dcterms:title>Implementing and Verifying MSC Specifications Using Promela/XSpin</dcterms:title> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:issued>1997</dcterms:issued> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:15Z</dc:date> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf 74

Das Dokument erscheint in:

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

KOPS Suche


Stöbern

Mein Benutzerkonto