CBabel Tool Prototype

CBabel Tool is a prototype executable environment for CBabel, that implements the CBabel's rewriting logic semantics and allows the execution and verification of CBabel descriptions in the Maude system, an implementation of rewriting logic.

Rewriting logic is a logic and semantic framework to which several models of computation, logics and specification languages have been mapped to due to its unified view of computation and logic. Maude is one implementation of rewriting logic that realizes it with high-performance. Together with its meta-programming facilities, the Maude system provides a rich tool for the development of formal tools. Moreover, Maude has built-in linear temporal logic model-checking capabilities and several verification tools. Another useful feature of the Maude language is its object-oriented syntax available as object-oriented modules.

The CBabel ADL has a very natural interpretation in object-oriented terms such as components as classes, component's instances as objects, port declarations as messages and port stimulus as message passing. The rewriting semantics that we have given to CBabel uses the object-oriented notation for rewriting logic and is implemented as a transformation function in Maude using its meta-programming capabilities. This transformation function is the core of the CBabel Tool execution environment prototype.

CBabel Tool Team

If you have any questions or comments, please email us at arademaker@ic.uff.br .

Downloading and Running CBabel Tool

The current version of CBabel Tool Prototype runs on Maude version 2.1.1, so you first need to download the Maude system and install it properly.

If you don't have Maude installed, download CBabel Tool with Maude here (1.3 Mbytes).
If you have already Maude installed in your system, download CBabel Tool without Maude files here (154 Kbytes).

To run the scripts below you must be running a Linux/Unix with bash or csh shell available.

Example 1 - Producer-Consumer-Buffer Synchronous

Execute the shell script demo-sync.sh with the command

sh demo-sync.sh

to load CBabel Tool with the synchronous version of producer and consumer modules and the architectures: pc-default (default connector), pc-mutex (mutual exclusive connector), pc-mutex-guards (mutual exclusive and guards connectors).

In Maude prompt you can now give the command below to verify all the architectures:

Maude> in s-examples/demo.maude

Or you may verify just one architecture (with mutual exclusive contract in that case) with the given interaction:

Maude> in s-examples/ver-pcbm.maude

and than

Maude> in s-examples/searches.maude

Example 2 - Producer-Consumer-Buffer Asynchronous

Execute the shell script demo-async.sh with the command

sh demo-async.sh

to load CBabel Tool with the asynchronous version of producer and consumer modules and the architectures: pc-default, pc-mutex, pc-mutex-guards.

In Maude prompt give the command

Maude> in a-examples/demo.maude

do verify all the architectures. (This will take about 40 minutes in a Pentium III 1 GHz with 1 GB RAM). Make sure that the maximum stack size available for the shell was set to unlimited before load the CBabel Tool.

To verify just one architecture (in that case, pc-mutex-guards) you can give the commands below:

Maude> in a-examples/ver-pcbmg.maude

and than

Maude> in a-examples/searches.maude