Database of Case Studies Achieved Using CADP

Access control in CORBA

Organisation: FernUniversität in Hagen

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed Systems.

Period: 1998

Size: 194,921 states and 1,149,090 transitions
84 lines of LOTOS

Description: CORBA, the Common Object Request Broker Architecture, specifies the interaction of objects in a distributed setting, hiding heterogeneity of components and providing transparency with respect to differences in data representation. However, object interfaces in CORBA are limited to the signature, leaving the behaviour unspecified. The authors propose to enhance the interfaces with behaviorual specification in the international standard LOTOS.

The case study tackles an access control system, controlling the access of a set of clients to a service in a distributed environment. Before accessing the service, a client must request permission from the access controller. The service contacts the access controller to check whether a client is authorized to access the service. Clients can also return access permissions.

The LOTOS specification of the access control was validated for a configurations with up to five clients and two simultaneous permission to access the service. For this configuration, the corresponding labeled transition system (194,921 states and 1,149,090 transitions) was generated in less than three minutes using less than 64 MB of RAM.

To gain confidence in the specification, the EXECUTOR and XSIMULATOR tools were used to simulate the specification and manually check the correctness of the observed execution traces. Using the EXHIBITOR tool, it was possible to obtain the shortest sequence leading to the granting of an access permission. Last, but not least, the EVALUATOR tool was used to model check two safety properties, namely that (1) a client is not granted the access to the service, unless it has been granted the permission beforehand, and (2) once a permission has been returned by a client, access to the service is not granted before a new permission is granted. For a configuration with three clients and two permissions, model checking took about one minute.

The specification has also been analysed using other formal techniques, in particular BDDs and CTL.

Conclusions: "Inspite of the limits we encountered in the use of foreign tools [...], the test and validation methods presented here and ongoing research work on better, in particular, compositional methods and tools, show a large potential for the prevention of design and implementation errors. Thus, the additional expenditure in the design phase can be justified by higher reliability and earlier fault prevention."

Publications: Bernd J. Krämer, Norbert Völker, Reiner Lichtenecker, and Hans-Friedrich Kötter. "Deriving Corba Applications from Formal Specifications". Journal of Systems Integration, 8, pp. 143-158, 1998.
Available on-line at:

Bernd Krämer

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Mon Jul 4 10:48:07 2022.

Back to the CADP case studies page