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.
If you have any questions or comments, please email us at firstname.lastname@example.org .
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.
To run the scripts below you must be running a Linux/Unix with bash or csh shell available.
Execute the shell script demo-sync.sh with the command
sh demo-sync.shto 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.maudeand than
Maude> in s-examples/searches.maude
Execute the shell script demo-async.sh with the command
sh demo-async.shto 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.maudedo 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.maudeand than
Maude> in a-examples/searches.maude