Publikation:

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

Vorschaubild

Dateien

Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdf
Formalization_and_validation_of_the_General_Inter_ORB_Protocol_GIOP_using_PROMELA_and_SPIN.pdfGröße: 266.6 KBDownloads: 705

Datum

2000

Autor:innen

Kamel, Moataz

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-62085
DOI (zitierfähiger Link)
https://doi.org/10.1007/s100090050045
ArXiv-ID

Internationale Patentnummer

Link zur Lizenz
Attribution-NonCommercial-NoDerivs 2.0 Generic

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published

Erschienen in

International journal on software tools for technology transfer. 2000, 2(4), pp. 394-409. Available under: doi: 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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

General Inter-ORB Protocol, Model checking, Promela/Spin, Temporal logic, Specification patterns

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690KAMEL, 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. 2000, 2(4), pp. 394-409. Available under: doi: 10.1007/s100090050045
BibTex
@article{Kamel2000Forma-5522,
  year={2000},
  doi={10.1007/s100090050045},
  title={Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN},
  number={4},
  volume={2},
  journal={International journal on software tools for technology transfer},
  pages={394--409},
  author={Kamel, Moataz and Leue, Stefan}
}
RDF
<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/server/rdf/resource/123456789/5522">
    <dc:language>eng</dc:language>
    <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"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:12Z</dc:date>
    <dc:format>application/pdf</dc:format>
    <dc:creator>Leue, Stefan</dc:creator>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5522"/>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <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>
    <dc:contributor>Kamel, Moataz</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:12Z</dcterms:available>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:bibliographicCitation>First publ. in: International journal on software tools for technology transfer 2 (2000), 4, pp. 394-409</dcterms:bibliographicCitation>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:issued>2000</dcterms:issued>
    <dc:creator>Kamel, Moataz</dc:creator>
    <dcterms:title>Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <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:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen