Bigraphs by Examples: A RESTful Vending Machine

This project is a template for building database-driven, object-oriented bigraphical applications
with execution logic defined by formally verified bigraphs. It bridges analysis and execution by using bigraphical model checking to verify system behavior before deployment.

Screenshots

Screenshot of the UI: The web UI allows interaction with the vending machine.	Screenshot of the CDO Explorer: Bigraphs are stored as Ecore models in a database.

Features

Bigraph-centric Design

• All application data and logic are modeled and stored as bigraphs (Ecore format) in a CDO-based in-memory database

Integration of Formal Verification

• The system behavior is subject to model checking
• Results of this analysis influence the application logic (e.g., web endpoints)

Reactive via Web Endpoints

• Bigraphical reactions (i.e. state transitions of the application) are triggered through RESTful API calls
• Ideal for interfacing with external systems or simulations

Model-Based State Evolution

• Design-time configuration: The initial state, rules, and predicates are set by placing the corresponding bigraph files in src/main/resources. These files are the output of formal analysis as implemented in Analysis.java.
• Runtime modification: The application behavior can be changed dynamically by editing the model in the CDO database (e.g., add a coin, or change the effect of a rule)

Getting Started

Requirements

• Java >=17
• Maven 3.8.7
• Spring 3.3.5
• Bigraph Framework 2.2.0
• BDSL 2.0.1
• CDO for Spring Data 0.7.5

Optional

• CDO Explorer: to view and modify the bigraph in the database
  1. Download CDO Explorer via the Eclipse Installer. Use Eclipse Version 2022-12 (4.26.0), which supports CDO protocol version 48. Eclipse IDE version 2023-09 supports only CDO protocol version 49.
  2. Any Eclipse IDE with CDO support, must support CDO protocol version 48

Via the IDE (Eclipse, IntelliJ IDEA, Visual Code, ...)

• Run the class src/main/java/org/example/Application.java
• Wait until you see in the terminal: "Application has successfully started ..."

Via the Terminal

Using Maven, issue the following command:

$ mvn clean package -DskipTests

The JAR file is created within the target folder of the project's root folder.

To run the application JAR file, execute the following command:

$ java -jar ./target/code-samples-1.0-SNAPSHOT.jar

# To change the server port
$ java -jar ./target/code-samples-1.0-SNAPSHOT.jar --server.port=9090

• Wait until you see in the terminal: Application has successfully started ...

Open the Browser

Afterward, open any browser and go to the following URL: http://localhost:8080/

If the bigraph doesn't appear to reflect the current state, simply refresh the page (press F5 or Ctrl+R) to update it.

Remarks

Database & Configuration

• The database configuration file is stored here: src/main/resources/config/cdo-server.xml
• Every time the application starts, a fresh in-memory CDO database is created
• The state of the program is not persisted, when the application is shut down
• Listeners for concrete objects in CDO can be attached before they are stored in the database (it is recommended to register listeners after)
  • See: VendingMachineObject and VMRuleSet

Analysis

• Analysis is placed in the ./src/test folder of this project

• Execute the unit tests to perform the analysis

• With the IDE or via Maven mvn -Dtest=Analysis test

• The results are stored in the resource folder

  • Rules, predicates and the metamodel

• The results are re-used for the implementation