KOPS - Das Institutionelle Repositorium der Universität Konstanz

Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN

Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:2dc0ed0840ed6e249c13cc79b8751de5

KAMEL, Moataz, Stefan LEUE, 2000. Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. In: International journal on software tools for technology transfer. 2(4), pp. 394-409. Available under: doi: 10.1007/s100090050045

@article{Kamel2000Forma-5522, title={Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN}, year={2000}, doi={10.1007/s100090050045}, number={4}, volume={2}, journal={International journal on software tools for technology transfer}, pages={394--409}, author={Kamel, Moataz and Leue, Stefan} }

<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/5522"> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:issued>2000</dcterms:issued> <dcterms:rights rdf:resource="https://creativecommons.org/licenses/by-nc-nd/2.0/legalcode"/> <dc:contributor>Leue, Stefan</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:12Z</dc:date> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5522/1/Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf"/> <dcterms:title>Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN</dcterms:title> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:12Z</dcterms:available> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5522/1/Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf"/> <dc:contributor>Kamel, Moataz</dc:contributor> <dc:creator>Leue, Stefan</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:creator>Kamel, Moataz</dc:creator> <dcterms:abstract xml:lang="eng">The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the servermigration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited.</dcterms:abstract> <dcterms:bibliographicCitation>First publ. in: International journal on software tools for technology transfer 2 (2000), 4, pp. 394-409</dcterms:bibliographicCitation> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:format>application/pdf</dc:format> <dc:rights>deposit-license</dc:rights> <dc:language>eng</dc:language> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5522"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf 184

Das Dokument erscheint in:

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

KOPS Suche


Stöbern

Mein Benutzerkonto