This page is dedicated to our tool CBA2Event-B plug-in.
To download the plug-in click here
To use our plug-in, you follow these steps :
1. Installation :
1.1 In the eclipse platform : Go to Help > Install New Software. Click Add
1.2 In the Name : tape the name of the plug-in, in the location you upload the plugin, then finish.
1.3 Right click on the project explorer , pointing to the composite file, the function translating to Event-B is added.
2. Use of our plug-in :
2.1 Select the composite file, right click, the CBA2EVENTB function will appear and then translate to event-B.
2.2 An Event-B project will be created.
2.3 If you have the rodin plug-in installed in your eclipse, you can verify the generated project . Else, you can use the rodin platform to verify and animate your example.
2.4 After generating the Rodin project you can generate the java code of the project by using the plugin Event-B2Java
For the ".composite" file, attached examples (standard), the composite file contains the assembly of components, and the interfaces (in java) contains the operations offered by the services.
Example 1 : Restaurant application
The restaurant component provides the menus proposed by the restaurant to clients through the RestaurantServiceComponent. The MenuService deployed by the MenuServiceComponent provides the menus descriptions and prices. The RestaurantServiceComponent allows to compute the bill for a particular menu. It interacts with the BillService provided by the BillServiceComponent through the billService reference interface to compute the price of a particular menu with the different taxes. In its turn, the BillServiceComponent collaborates with the VatServiceComponent that computes the VAT (Value Added Tax) and with the TipServiceComponent that computes the tip. More informations about this cas study can be found here. The composite implementation can be found via this link : Restaurant application code.
Example 2 : Calculator application
The Calculator composite is composed of five components. Calculator Service Component receives requests to call one of the basic calculation operations. Its front-end service "Calculator service" is promoted by the composite. The calculator component calls the four basic calculation components via its references, i.e. AddReference, SubtractReference, MultiplyReference and DivideReference. Add Service Component computes the sum of two double type input variables. This functionality is provided by its AddService service. Subtract Service Component computes the difference between two input double variables. This functionality is presented by its SubtractService service. Multiply Service component performs the multiplication operation through its MultiplyService interface. Divide Service component divides the first double variable by the second one. This component is accessible via its DivideService service. The composite implementation can be found via this link : Calculator application code.
Example 3 : Where dinner Composite Service application
This application provides the nearest restaurant to the client location. It is made up of four components. The Parking Service Component implements the Parking Service. The Fuel Service Component provides the Fuel Service which is used by the Restaurant Menu Service Component and invokes from the service provided by the Location Service Component. The Location Service Component provides the Location Service and some functionalities to the Fuel Service Component and Restaurant Menu Service Component. The Restaurant Menu Service Component is the main component that uses all the services provided by other components. The composite implementation can be found via this link : Where dinner Service code.
Authors: Amel Mammar (amel.mammar@telecom-sudparis.eu) -Lazhar Hamel (lazhar.hamel@gmail.com) -Mohamed Graiet (mohamed.graiet1@gmail.com) -