Skip to content

Commit

Permalink
Updated README
Browse files Browse the repository at this point in the history
  • Loading branch information
@fynndemmler
fynndemmler committed Nov 14, 2023
1 parent 6256104 commit 1ea01f1
Showing 1 changed file with 75 additions and 42 deletions.
117 changes: 75 additions & 42 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,58 +4,91 @@ Tool Support for Correctness-by-Construction
# [C-CorC](https://github.com/KIT-TVA/CorC/wiki/CorC-for-Information-Flow)
Tool Support for Confidentiality- and Correctness-by-Construction

# CorC Project Setup Guide & Case Study Introduction (2023-11-09)
# <span style="color:#007A61">CorC Setup Guide & Case Study Introduction (2023-11-14)</span>
Installation guide for plugins and properties for **development with CorC** with introduction of case studies.
## Java Version
* Please use [**JDK 16**](https://www.oracle.com/java/technologies/javase/jdk16-archive-downloads.html). CorC may not work out of the box with newer versions.
## Setup
### **Plugins and Software**
* **Eclipse** Install [Eclipse Modelling Tools](https://www.eclipse.org/downloads/packages/release/2023-09/r). Please use version 2023-09 (Eclipse 4.29.0). CorC may not work correctly with other versions.
* Before installing any plugins, navigate to *Preferences > Install/Update > Available Software Sites* and disable *Latest Eclipse IDE Packages Release* and *Latest Eclipse Simultaneous Release*.
* **Graphiti** Install Graphiti using the update site https://download.eclipse.org/graphiti/updates/0.18.0/
* **KeY** Install KeY using the update site https://formal.iti.kit.edu/key/download/releases/2.6/eclipse/ (disable *Group items* to show available plugins, install all)
* **Xtext** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/eclipse-xtext)
* **FeatureIDE** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/featureide)
* **Mylyn** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/mylyn) (Mylyn 3.23)
* **TestNG** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/testng-eclipse)
* **Z3** Get the latest release of [Z3](https://github.com/Z3Prover/z3/releases) and add it to the environment variable [PATH](https://www.wikihow.com/Change-the-PATH-Environment-Variable-on-Windows).

## Properties & Initialisation
1. Checkout master from https://github.com/TUBS-ISF/CorC.git
2. Install **JaMoPP** using the two plugins of the tool.update package from Git (disable *Group items* to show available plugins)
## <span style="color:#007A61">Java Version</span>
Please use [**JDK 16**](https://www.oracle.com/java/technologies/javase/jdk16-archive-downloads.html). CorC may not work out of the box with newer versions.
## <span style="color:#007A61">Setup</span>
### Software
> Install [Eclipse Modelling Tools](https://www.eclipse.org/downloads/packages/release/2023-09/r) (Version 2023-09).

### **Plugins**
- **Graphiti** Install Graphiti using the update site https://download.eclipse.org/graphiti/updates/0.18.0/

- **KeY** Install KeY using the update site https://formal.iti.kit.edu/key/download/releases/2.6/eclipse/ (disable *Group items* to show available plugins, install all)

- **Xtext** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/eclipse-xtext)

- **FeatureIDE** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/featureide)

- **Mylyn** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/mylyn) (Mylyn 3.23)

- **TestNG** Available in [Eclipse Marketplace](https://marketplace.eclipse.org/content/testng-eclipse)

- **Z3** Get the latest release of [Z3](https://github.com/Z3Prover/z3/releases) and add it to the environment variable [PATH](https://www.wikihow.com/Change-the-PATH-Environment-Variable-on-Windows).

## <span style="color:#007A61">Properties & Initialisation</span>
1. Clone the repo:
```sh
git clone https://github.com/KIT-TVA/CorC.git
```
2. Install **JaMoPP** using the two plugins inside package *\*.tool.update* (disable *Group items* to show available plugins).
3. Open the following packages in Eclipse Modelling Tools:
* de.tu-bs.cs.isf.cbc.model
* de.tu-bs.cs.isf.cbc.tool
* de.tu-bs.cs.isf.cbc.util
* de.tu-bs.cs.isf.cbcclass.tool
* de.tu-bs.cs.isf.wizards
* de.tu_bs.cs.isf.cbc.parser
* de.tu_bs.cs.isf.cbc.statistics
* de.tu_bs.cs.isf.cbc.statistics.ui
* de.tu_bs.cs.isf.commands.toolbar
* de.tu_bs.cs.isf.lattice

4. Generate model/edit/editor: Open model/genmodel.genmodel of package cbc.model and model/cbcstatistics.genmodel of package cbc.statistics and rightclick on Generate model/edit/editor. If multiple resolving errors occur, uninstall JaMoPP Plugins via Window -> Preferences -> Install/Update -> Uninstall or update. After uninstalling, reinstall as described above.
5. Select any package and run project as Eclipse Application.

## Examples and Case Studies
- de.tu-bs.cs.isf.cbc.model
- de.tu-bs.cs.isf.cbc.tool
- de.tu-bs.cs.isf.cbc.util
- de.tu-bs.cs.isf.cbcclass.tool
- de.tu-bs.cs.isf.wizards
- de.tu_bs.cs.isf.cbc.parser
- de.tu_bs.cs.isf.cbc.statistics
- de.tu_bs.cs.isf.cbc.statistics.ui
- de.tu_bs.cs.isf.commands.toolbar
- de.tu_bs.cs.isf.lattice

4. *Right click -> Generate Model/Edit/Editor Code* in **all** of the following files:
- *\*.cbc.model -> model -> cbcmodel.genmodel*
- *\*.cbcclass.model -> model -> cbcclass.genmodel*
- *\*.cbc.statistics -> model -> cbcstatistics.genmodel*

5. Select any package and run project as *Eclipse Application*.

## <span style="color:#007A61">Examples and Case Studies</span>
We provide different examples and case studies to explore CorC!
### Examples
Create CorC-examples via File -> New -> Other... -> CorC -> CorC Examples -> Select examples you want to create.
Create CorC-examples via *File -> New -> Other... -> CorC -> CorC Examples ->* Select examples you want to create.
### Case studies
The repository you checked out contains various software product line case studies. They can be loaded via File -> Open project from file system.
The repository you checked out contains various software product line case studies. They can be loaded via *File -> Open project from file system*.
#### BankAccount
The BankAccount implements basic functions of a bank account such as withdrawals, limits, money transfers and checking the account balance.
* **BankAccount** Object-oriented implementation with class structure and CbC-Classes.
* **BankAccountOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
- **BankAccount** Object-oriented implementation with class structure and CbC-Classes.
- **BankAccountOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
#### Elevator
The Elevator implements basic functions of an elevator such as the movement and entering and leaving of persons.
* **Elevator** Object-oriented implementation with class structure and CbC-Classes.
- **Elevator** Object-oriented implementation with class structure and CbC-Classes.
#### Email
The product line Email implements basic functions of an email system including server- and client-side interactions.
* **EmailOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
* **EmailFeatureInteraction** Java-Implementation without implementation with CbC.
- **EmailOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
- **EmailFeatureInteraction** Java-Implementation without implementation with CbC.
#### IntegerList
The IntegerList implements a list of integers with add and sort operations.
* **IntegerList** Object-oriented implementation with class structure and CbC-Classes.
* **IntegerListOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
- **IntegerList** Object-oriented implementation with class structure and CbC-Classes.
- **IntegerListOO** Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.

## <span style="color:#007A61">Common Issues</span>

**Problem:** Multiple resolving errors after generating model files.

**Solution:** Uninstall JaMoPP Plugins via *Window -> Preferences -> Install/Update -> Uninstall or update*. Afterwards reinstall as described above.

---

**Problem:** Cycling depedency issues.

**Solution:** Navigate to: *Project -> Properties -> Java Compiler -> Building -> Configure Workspace Settings -> Build path problems -> Circular dependencies* and set the listbox to *Warning*.

---

**Problem:** Errors in certain files about undefined methods and classes.

**Solution:** Changing the compliance: *Project -> Java Compiler -> JDK Complicance -> Use compliance from execution environment 'JavaSE-16'*.

0 comments on commit 1ea01f1

Please sign in to comment.