@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
    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>