Title :
Specification and verification of an object request broker
Author_Institution :
Comput. Networking Lab., Ecole Polytech. Fed. de Lausanne, Switzerland
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;
Conference_Titel :
Software Engineering, 1998. Proceedings of the 1998 International Conference on
Conference_Location :
Kyoto
Print_ISBN :
0-8186-8368-6
DOI :
10.1109/ICSE.1998.671101
