We give a formal specification and analysis of the security service of CORBA, the Common Object Request Broker Architecture specified by the Object Management Group, OMG. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, committee-designed, informal specification. Our approach is scenario-driven: we use representative scenarios to determine which parts of the informal specification should be formalized and verify the resulting formal specification against these scenarios. For the formalization, we have speci.ed a significant part of the security service’s data-model using the formal language Z. Through this process, we have been able to sharpen the OMG-specification, uncovering a number of errors and omissions.

A Formal Analysis of the CORBA Security Service

VIGANO', Luca
2002

Abstract

We give a formal specification and analysis of the security service of CORBA, the Common Object Request Broker Architecture specified by the Object Management Group, OMG. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, committee-designed, informal specification. Our approach is scenario-driven: we use representative scenarios to determine which parts of the informal specification should be formalized and verify the resulting formal specification against these scenarios. For the formalization, we have speci.ed a significant part of the security service’s data-model using the formal language Z. Through this process, we have been able to sharpen the OMG-specification, uncovering a number of errors and omissions.
3540431667
Formal methods; Middleware; Z language
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/243771
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact