KOPS - Das Institutionelle Repositorium der Universität Konstanz

Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract

Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:27d4ed574149287b3edc73bc8e888ccc

LEUE, Stefan, Peter B. LADKIN, 1996. Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract. SPIN. Rutgers University, New Brunswick, New Jersey, Aug 1996. In: Participants Proceedings of the Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey, August 1996. SPIN. Rutgers University, New Brunswick, New Jersey, Aug 1996

@inproceedings{Leue1996Imple-5462, title={Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract}, year={1996}, booktitle={Participants Proceedings of the Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey, August 1996}, author={Leue, Stefan and Ladkin, Peter B.} }

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/5462"> <dc:creator>Ladkin, Peter B.</dc:creator> <dc:creator>Leue, Stefan</dc:creator> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:36Z</dc:date> <dc:language>eng</dc:language> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5462"/> <dcterms:bibliographicCitation>First publ. as paper in: Participants Proceedings of the Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey, August 1996</dcterms:bibliographicCitation> <dc:format>application/pdf</dc:format> <dcterms:title>Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin : Extended Abstract</dcterms:title> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:rights rdf:resource="https://creativecommons.org/licenses/by-nc-nd/2.0/legalcode"/> <dcterms:abstract xml:lang="eng">In previous work we defined a finite state semantics for Message Sequence Charts (MSCs) and suggested a translation of MSC specifications into Promela. We call this translation an 'implementation'. In this paper we reconsider the implementation of MSCs and discuss what information needs to be added when implementing MSC specifications containing so-called nonlocal choices. Next, we show how to model-check liveness requirements imposed on MSC specifications. We use 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> <dcterms:issued>1996</dcterms:issued> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:36Z</dcterms:available> <dc:rights>deposit-license</dc:rights> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Implementing_and_Verifying_Scenario_Based_Specifications_Using_Promela.pdf 62

Das Dokument erscheint in:

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

KOPS Suche


Stöbern

Mein Benutzerkonto