Specification and verification of an object request broker

Author

Duval, Grégory

Author_Institution

Comput. Networking Lab., Ecole Polytech. Fed. de Lausanne, Switzerland

fYear

1998

fDate

19-25 Apr 1998

Firstpage

43

Lastpage

52

Abstract

This paper reports the results of specifying, modeling and verifying a safe object request broker. This method has been applied on several case studies by using the SPIN verification tool. An object request broker has been implemented using sC++, a concurrent extension of C++ designed by our team. Liveness and safety properties have been checked on the model to ensure the system behaviour is correct. This application shows the efficiency of using formal methods in building safe applications. It also shows that sC++ is appropriate for developing protocols and communicating systems and is easily translatable from models such as Promela

Keywords

client-server systems; formal specification; object-oriented languages; object-oriented methods; program verification; temporal logic; C++; CORBA; Promela; SPIN verification tool; case studies; communicating systems; concurrent extension; formal methods; liveness; modeling; object request broker specification; object request broker verification; protocols; sC++; safety properties; system behaviour; temporal logic; Buildings; Computer architecture; Computer networks; Concurrent computing; Laboratories; Logic; Protocols; Safety; Space exploration; State-space methods;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering, 1998. Proceedings of the 1998 International Conference on

Conference_Location

Kyoto

ISSN

0270-5257

Print_ISBN

0-8186-8368-6

Type

conf

DOI

10.1109/ICSE.1998.671101

Filename

671101