Tool Support for Correctness-by-Construction
Tool Support for Confidentiality- and Correctness-by-Construction
Installation guide for plugins and properties for development with CorC with introduction of case studies.
- Eclipse Install Eclipse Modelling Tools. Please use version 2021-06 (Eclipse 4.20.0). CorC may not work correctly with newer versions.
- 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/
- Xtext Available in Eclipse Marketplace
- Jamopp Available in Eclipse Marketplace
- FeatureIDE Available in Eclipse Marketplace
- Mylyn Available in Eclipse Marketplace (Mylyn 3.23)
- Checkout master from https://github.com/TUBS-ISF/CorC.git
- Open the following packages in Eclipse Modelling Tools:
- de.tu_bs.cs.isf.cbc.cbcclass.model
- 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.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
- Disable warnings for circular dependencies: Window -> Preferences -> Java -> Compiler -> Building -> Build path problems -> Circular dependencies -> Warning
- Generate model/edit/editor: Open model/.genmodel of cbcmodel, cbcclassmodel, and statistics and rightclick on Generate ... If multiple referencing errors occur, uninstall Jamopp Plugins via Window -> Preferences -> Install/Update -> Uninstall or update. After uninstalling, reinstall via Marketplace.
- Select any package and run project as Eclipse Application.
We provide different examples and case studies to explore VarCorC!
Create CorC-examples via File -> New -> Other... -> CorC -> CorC Examples -> Select examples you want to create.
The repository you checked out contains various software product line case studies. They can be loaded via File -> Open project from file system.
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.
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.
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.
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.