Abstract:

A Formal Data-Model of the CORBA Security Service

David Basin and Frank Rittinger and Luca Viganò


We use the formal language Z to specify and analyze the security service of CORBA. 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, informal specification. Our approach is scenario-driven: we use representative scenarios to determine 
which parts of the informal specification should be formalized and then verify the formal specification against the
requirements of these scenarios.