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

Moataz Kamel | Zendy; Stefan Leue | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Moataz Kamel,

Stefan Leue

Publication year - 2000

Publication title -

international journal on software tools for technology transfer

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.397

H-Index - 55

eISSN - 1433-2787

pISSN - 1433-2779

DOI - 10.1007/s100090050045

Subject(s) - promela , computer science , common object request broker architecture , model checking , programming language , protocol (science) , formal verification , linear temporal logic , formal specification , theoretical computer science , medicine , alternative medicine , pathology

The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Bro- ker Architecture (CORBA) specication. 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 specication. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. Dur- ing the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specication patterns helped us in formalizing the high-level requirements that we have elicited.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research