|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: https://doi.org/10.1023/A:1008226622237 |
| Contact: | Bernd Krämer Email: bernd.kraemer@fernuni-hagen.de |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page