Publikation:

Implementing and Verifying MSC Specifications Using Promela/XSpin

Vorschaubild

Dateien

Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf
Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdfGröße: 327.62 KBDownloads: 347

Datum

1997

Autor:innen

Ladkin, Peter B.

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-65136
DOI (zitierfähiger Link)
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

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. Providence: American Mathematical Society, 1997

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

DIMACS, 5. Aug. 1996
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690LEUE, 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. Providence: American Mathematical Society, 1997
BibTex
@inproceedings{Leue1997Imple-5423,
  year={1997},
  title={Implementing and Verifying MSC Specifications Using Promela/XSpin},
  publisher={American Mathematical Society},
  address={Providence},
  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: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/5423">
    <dc:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights>
    <dcterms:title>Implementing and Verifying MSC Specifications Using Promela/XSpin</dcterms:title>
    <dc:creator>Ladkin, Peter B.</dc:creator>
    <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:contributor>Ladkin, Peter B.</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5423/1/Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5423/1/Implementing_and_Verifying_MSC_Specifications_Using_PromelaXSpin.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:language>eng</dc:language>
    <dcterms:issued>1997</dcterms:issued>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:15Z</dcterms:available>
    <dc:format>application/pdf</dc:format>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5423"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:15Z</dc:date>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <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>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/>
  </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
Nein
Begutachtet
Diese Publikation teilen