KIT | KIT-Bibliothek | Impressum | Datenschutz

Quantification of Correctness with Palladio and KeY: Case Study Data

Reiche, Frederik; Schiffl, Jonas; Weigl, Alexander

Abstract (englisch):
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.

Open Access Logo


Zugehörige Institution(en) am KIT Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Institut für Theoretische Informatik (ITI)
Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Forschungsdaten
Publikationsdatum 01.02.2021
Erstellungsdatum 13.03.2020 - 19.08.2020
Identifikator DOI (KIT): 10.5445/IR/1000129008
KITopen-ID: 1000129008
Lizenz Creative Commons Namensnennung – Weitergabe unter gleichen Bedingungen 4.0 International
Projektinformation KASTEL_SKI (BMBF, 16KIS0843)
Vorab online veröffentlicht am 26.01.2021
Liesmich

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.

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.

Art der Forschungsdaten Dataset
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page