DocumentCode :
2877990
Title :
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
Link To Document :
بازگشت