KOPS - The Institutional Repository of the University of 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

Cite This

Files in this item

Checksum: 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:rights>terms-of-use</dc:rights> <dc:format>application/pdf</dc:format> <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>

Downloads since Oct 1, 2014 (Information about access statistics)

Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf 304

This item appears in the following Collection(s)

terms-of-use Except where otherwise noted, this item's license is described as terms-of-use

Search KOPS


Browse

My Account