Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN
| Type of Publication: | Journal article |
| URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-62085 |
| Author: | Kamel, Moataz; Leue, Stefan |
| Year of publication: | 2000 |
| Published in: | International journal on software tools for technology transfer ; 2 (2000), 4. - pp. 394-409 |
| DOI (citable link): | https://dx.doi.org/10.1007/s100090050045 |
| Summary: |
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.
|
| Subject (DDC): | 004 Computer Science |
| Keywords: | General Inter-ORB Protocol, Model checking, Promela/Spin, Temporal logic, Specification patterns |
| Link to License: | In Copyright |
Cite This
Files in this item
![[PDF]](/themes/Kops/images/mimes/pdf.png "PDF file"){kind=small}
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 | 362 |
This item appears in the following Collection(s)
Except where otherwise noted, this item's license is described as terms-of-use
Search KOPS
Browse
My Account
