Menu ▾ ▴

Home

Tim Wahls

About EventB2SQL

EventB2SQL is a tool for translating Event-B models to Java database applications (implemented using JDBC and MySQL or SQLite), Android applications (using the Android-native SQLite API), and PHP applications (using PDO and MySQL). It can translate Event-B models written at a high level of abstraction, and translating to database applications provides data persistence and allows the implementation to be used as a client-server application with minimal additional effort. EventB2SQL is implemented as a plugin for Rodin and has been tested under Linux and MacOS.

Installation

  1. Install Rodin: https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.2/ EventB2SQL only works with Rodin 3.2.
  2. Start Rodin.
  3. Go to Help, then Install New Software.
  4. Add software site:

http://users.dickinson.edu/~wahlst/EventB2SQL-update

select EventB2SQL and click Next.
5. On the Install Details page, click Next again, then accept the (empty) license agreement.
6. Click Finish, and then OK at the security warning.

Generating Code

From the Event-B Explorer pane in Rodin, right-click on the machine that you wish to translate and select the translation target:

  • Translate to MySQL
  • Translate to SQLite (JDBC)
  • Translate to SQLite (Android)
  • Translate to MySQL (PHP)

The first three options generate Java code, while the fourth generates PHP. For all four options, the generated code is placed in the generated_sql directory within the Rodin project by default, but this can be edited in the "Output File" pop-up. For the three Java options, the user can then enter a package for the generated class. For all options, the generated code consists of a single class with the same name as the machine.

Using the Generated Code

MySQL (JDBC)

  1. Install MySQL Connector/J: http://dev.mysql.com/downloads/connector/j/ and add the jar file to your classpath (if you have not already done so).
  2. Download eventB2SQL.jar: http://users.dickinson.edu/~wahlst/eventb2sql/eventB2SQL.jar and add it to your classpath.
  3. Within MySQL, create a new database and a user with full permissions on that database (or choose an existing database and user). The rest of this section assumes that the database is called eventb, the user is ebuser and the password is pass.

  4. Write a driver program to use the class generated by EventB2SQL. Note that the constructor for the generated class takes a database connection as its parameter. If your generated class is Test.java, machine Test uses no carrier sets, and you named your database and user as mentioned above, the following should work:

    Class.forName("com.mysql.jdbc.Driver");
    Connection con;
    con = DriverManager.getConnection("jdbc:mysql://localhost/eventb?&autoDeserialize=true", "ebuser", "pass");
    Test test = new Test(con);
    test.createTables();
    test.INITIALISATION();

  5. The createTables method should be called only once (to create the database tables used by the implementation), while INITIALISATION can be called at any point to reset machine variables to their initial values. If machine that you translated sees any contexts that use given sets, the createTables method takes additional parameters containing the initial values of each of those sets.

  6. Add more code to call the methods in the generated class as desired.

SQLite (JDBC)

  1. Download the jar file containing the JDBC driver for SQLite: https://bitbucket.org/xerial/sqlite-jdbc/downloads and add it to your classpath (if you have not already done so).
  2. Download eventB2SQL.jar: http://users.dickinson.edu/~wahlst/eventb2sql/eventB2SQL.jar and add it to your classpath.

  3. Write a driver program to use the class generated by EventB2SQL. Note that the constructor for the generated class takes a database connection as its parameter. If your generated class is Test.java, machine Test uses no carrier sets, and you named your database and user as mentioned above, the following should work (note that the database is stored in file sample.db):

    Class.forName("org.sqlite.JDBC");
    Connection con;
    con = DriverManager.getConnection("jdbc:sqlite:sample.db");
    Test test = new Test(con);
    test.createTables();
    test.INITIALISATION();

  4. The createTables method should be called only once (to create the database tables used by the implementation), while INITIALISATION can be called at any point to reset machine variables to their initial values. If machine that you translated sees any contexts that use given sets, the createTables method takes additional parameters containing the initial values of each of those sets.

  5. Add more code to call the methods in the generated class as desired.

SQLite (Android)

  1. Download eventB2SQL.jar: http://users.dickinson.edu/~wahlst/eventb2sql/eventB2SQL.jar
  2. Copy eventB2SQL.jar to the app/libs directory of your Android Studio project.
  3. From the Build menu in Android Studio, select Rebuild Project (so the project finds the jar that you copied in the previous step).
  4. Place the code generated by EventB2SQL in the appropriate package in the Java source of your Android Studio project.

  5. The constructor for the generated class takes the context for your application as a parameter. This can be obtained by calling:

    this.getApplicationContext()

  6. After creating an instance, use it to call the createTables, INITIALISATION and other methods in the generated class as specified in the previous two sections.

MySQL (PHP PDO)

  1. If the model you generated PHP code for contains any carrier sets, implement a PHP classes for each with exactly the same name and include those classes in your application.

  2. The constructor for the generated class takes a database connection as a parameter. If you have created a MySQL database and user as specified in the MySQL (JDBC) section above and translated a machine called Test, the following should work:

    $con = new PDO("mysql:host=localhost;dbname=eventb", "ebuser", "pass",
    array(PDO::ATTR_EMULATE_PREPARES => false,
    PDO::ATTR_ERRMODE => PDO::ERRMODE_EXCEPTION));
    $tst = new Test($con);
    $tst->dropTables();
    $tst->createTables();
    $tst->INITIALISATION();

  3. The createTables method should be called only once (to create the database tables used by the implementation), while INITIALISATION can be called at any point to reset machine variables to their initial values. If machine that you translated sees any contexts that use given sets, the createTables method takes additional parameters containing the initial values of each of those sets (as arrays).

  4. Add more code to call the methods in the generated class as desired.

Social Networking Example

Java (non-Android)

  1. Download http://users.dickinson.edu/~wahlst/eventb2sql/SocialNetworkCaller.zip and either import it into an Eclipse project or unzip it (if you will compile and run the example from the command line or another IDE).
  2. Add eventB2SQL.jar and the appropriate database driver jar file to your Build Path/CLASSPATH as described above.
  3. Download http://users.dickinson.edu/~wahlst/eventb2sql/SocialNetworking.zip and unzip it in your Rodin workspace.
  4. Start Rodin and create an Event-B project called SocialNetworking. Rodin will create the project using the files from the previous step.
  5. Refresh your new project.
  6. Translate the machine ref0_abstract as described above, entering the path to place ref0_abstract.java into the directory containing the files from Step 1.
  7. If using Eclipse, refresh your project so that Eclipse will recognize ref0_abstract.java.
  8. In the main method of class SocialNetworkCaller, set variable SQLite to true if you are using SQLite, and false if you are using MySQL. If you are using MySQL, adjust the database name, database user and password to match your setup.
  9. Run class SocialNetworkCaller. Note that you should create three users before using the transmit option.

Android

  1. Create a new Android Studio project called SocialNetwork with a blank main activity in package edu.dickinson.socialnetwork.
  2. Download and unpack http://users.dickinson.edu/~wahlst/eventb2sql/AndroidExample.zip. Copy the files in AndroidExample/java to the app/src/main/java/edu/dickinson/socialnetwork directory in your new project.
  3. Copy the files in AndroidExample/layout to the app/src/main/res/layout directory in your new project.
  4. Copy the file in AndroidExample/manifest to the app/src/main directory in your new project.
  5. Copy eventB2SQL.jar to the app/libs directory of your project (if you haven't already done so).
  6. Set up the SocialNetworking project in Rodin as described in the previous section, and translate machine ref0_abstract to SQLite (Android). Place the generated code in the app/src/main/java/edu/dickinson/socialnetwork directory in your Android Studio project, and enter edu.dickinson.socialnetwork as the package. (Note that AndroidExample.zip already contains a translation, so you can skip this step if you wish.)
  7. From the Build menu in Android Studio, select Rebuild Project
  8. Run the project.
  9. In your device or emulator, click the CREATE DATABASE button to create the database.
  10. Enter a person's name or content of a post before clicking ADD PERSON or ADD CONTENT.
  11. Use the CREATE ACCOUNT button to create accounts.
  12. The entire current state of the network is always displayed on the app.

app interface

Project Members: