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.

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.