Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN
- Startseite
- →
- Informatik und Informationswissenschaft
- →
- Informatik und Informationswissenschaft
- →
- Dokumentanzeige
| Publikationstyp: | Zeitschriftenartikel |
| URI (zitierfähiger Link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-62085 |
| Autor/innen: | Kamel, Moataz; Leue, Stefan |
| Erscheinungsjahr: | 2000 |
| Erschienen in: | International journal on software tools for technology transfer ; 2 (2000), 4. - S. 394-409 |
| DOI (zitierfähiger Link): | https://dx.doi.org/10.1007/s100090050045 |
| Zusammenfassung: |
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.
|
| Fachgebiet (DDC): | 004 Informatik |
| Schlagwörter: | General Inter-ORB Protocol, Model checking, Promela/Spin, Temporal logic, Specification patterns |
| Link zur Lizenz: | Nutzungsbedingungen |
Zitieren
Dateien zu dieser Ressource
![[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>
Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)
| Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf | 233 |
Das Dokument erscheint in:
Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: terms-of-use
KOPS Suche
Stöbern
Mein Benutzerkonto
