Specification and Verification of an Object Request Broker

DOI 10.1109/icse.1998.671101 dblp

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.

BibTeX

@inproceedings{Duval:ICSE98,
  author    = {Gr{\'{e}}gory Duval},
  title     = {Specification and Verification of an Object Request Broker},
  booktitle = {ICSE},
  pages     = {43--52},
  publisher = {{IEEE} Computer Society},
  year      = {1998},
}

Specification and Verification of an Object Request Broker

Abstract

Related papers