Alternate identifier:
(KITopen-DOI) 10.5445/IR/1000129008
Related identifier:
Reiche, Frederik [Reiche, Frederik]

Schiffl, Jonas [Schiffl, Jonas]

Weigl, Alexander [Weigl, Alexander]
Quantification of Correctness with Palladio and KeY: Case Study Data
Additional titles:
(Abstract) In our report, we described a case study where we evaluate our approach for correctness quantification using Palladio and KeY. Here, we publish the corresponding Palladio Component Model files as well as the generated source code, in order to make them publicly available.
(Technical Remarks) # README: Case Study (Age of Maturity) This archive contains the Palladio artifacts of the case study "AgeOfMaturity" of the Technical-Report "Model-driven Quantification of Correctness with Palladio and KeY" (DOI: 10.5445/IR/1000128855). The structure of this archive is as follows: * The folder "PalladioModels" contains the Palladio Component Model Eclipse Project of the "AgeOfMaturity" use case * The folder "DependencySolverResults" contains output files with the results of the solved "AgeOfMaturity" case study as described in the report * The folder "GeneratedJavaCode" contains Java-Code generated with the [PCM2Java]( Project * The folder "PalladioDiagrams" contains the exported model diagrams of the "AgeOfMaturity" case study created for the technical report The usage of the Palladio Editor and the DependencySolver is explained in the following. ## Setup For usage of the artifacts, an Eclipse IDE with the installed Palladio Simulator is necessary. * Download and run a clean [Release of the **Eclipse Modeling Tools** 2020-06 IDE]( * Install the Palladio Simulator by using the [Eclipse Market Place]( or the [Palladio Update Site]( Install at least the Palladio Component Model, the "Analyzer: Analytical Solver" and the Editors. ## Viewing and Modifying the Models * Import the Palladio AgeOfMaturity Project: * Open the Import Window in Eclipse (File --> Import --> General --> Existing Projects into Workspace) * In the opened Import Windows select the path to the "edu.kit.kastel.scbs.ageofmaturity" Project in the PalladioModels Folder. * Select "Finish" * Open the files with the suffix "_diagram", to view the models with the installed GMF Editors. ## Running the DependencySolver * Create a PCM Solver Run Configuration: (Run --> Run Configurations --> Call Context Menu for PCM Solver --> New Configuration) * Select the created Run Configuration * Configure Architecture Models in the Configuration (Select "Architecture Model(s)" Tab) * Insert Configuration Name * Under "Allocation File" insert the AgeOfMaturity.allocation file path (e.g. by using the "Workspace..." menu) * Under "Usage File" insert the AgeOfMaturity.allocation File Path (e.g. by using the "Workspace..." menu) * Configure the Solver (Select "Solver" Tab) * Select "SRES (Stochastic Regular Expression Solver)" * Uncheck "Use of Expression Model File" checkbox * Provide Path to an Output file in "Expression Model File" * Optional: Configure the Analysis to store Temporary Data(Select "Analysis Configuration" Tab) * Provide Location for storing the temporal data: Under "Location of temporary data", uncheck "use default location" checkbox and provide path to the location * Uncheck the "Delete temporary data after analysis" checkbox. ## Result Interpretation The computed usage/output shows the folded probabilities for each branch in the usage scenario and the visited service effect specifications. The probability to enter a critical section (see technical report) under the given usage model can be retrieved through inspection of the entries for the inserted branches for the critical sections.
Related information:
Production year:
Subject areas:
Computer Science
Resource type:
Data source:
Software used:
Data processing:
Publication year:
Rights holders:
Reiche, Frederik
Name Storage Metadata Upload Action

Number of views in the previous six months.

Dataset page views




Overall statistics

Period Landing page accessed Dataset downloaded
Dec 2023 2 0
Nov 2023 20 0
Oct 2023 9 0
Sep 2023 3 0
Aug 2023 11 0
Jul 2023 5 0
Before 13 0
Total 63 0
Uploaded by:
Created on:
Archiving date:
Archive size:
479.7 kB
Archive creator:
Archive checksum:
cf64537c4ab9bd6bf2ca7cc891621008 (MD5)
Embargo end date: