SoS Goal Model Slicer

Background

The verification property detection tools related to the SoS change use the SoS target model slicing technique and the model based statistical verification technique. The SoS target model slicing technique is a technique to perform backward slicing from the target of the configuration system related to the change to the upper target in the target model of the tree type created by the SoS manager. The model-based statistical verification technique obtains as a sample whether the verification property, that is, whether each target in the target model has been achieved in a plurality of independent model runs, and then uses the statistical hypothesis test on the observed sample to determine whether the verification property of the entire system satisfies Is quantitatively / statistically determined.

As the number of iterations increases, the accuracy of the verification result increases as the sample set approaches the sum total. However, statistical verification based on simulation takes a long time to perform verification. In other words, verifying targets in the target model every time a change occurs in the SoS means that the time and cost are much greater. Performing a verification using a verification property detection tool related to the SoS change helps to reduce the verification cost. At this time, the verification property detection tool related to the SoS change must accurately detect the target related to the change so that the cost can be reduced without performing additional verification. Therefore, we want to ensure the reliability of the tool by examining the accuracy of detection of the verification properties related to changes in the tool.

 

Tool Overview: SoS Goal Model Slicer

 

  • User Interface

  • Tool Features
  1. Select or enter verification property related to the change in the tool’s input window.
  2. Represent the SoS goal model on the output window
  3. Perform the reverse slicing according to the slicing criterion of the dependency of the SoS target model.
  4. Show the SoS goal model slicing results on the output window.

 

Opensource Repository

<Goal Model Slicer> module is included in <SIMVA-SoS>

GitHub link: https://github.com/SESoS/SIMVA-SoS

 

Installation Guide

[Preparation]

You need to install following environment to run our SIMSoS:

  • JVM 1.8 or later
  • Gradle 3.1 or later

We recommend that you install IntelliJ to run our tool easier.

[Process]

  1. Checkout our SIMVA-SoS where you want it installed.
  • $ git clone https://github.com/SESoS/SIMVA-SoS.git
  1. You have two options, load the project using gradle and IntelliJ. If you choose this, you just use File > New > Project from Version Control > GitHub and type our repository location. If you already downloaded our project, you just import it.

 

User Manual

1. run program in IntelliJ by clicking right-button of mouse on SIMVA-SoS.Slicing.src.goalModelSlicer.Main in SIMVA-SoS project

2. Prepare a slicing tool and two input files, a target model file (.csv) and a slice-based text file (.txt).

3. Enter the model file in the first input box on the upper left input of the tool. If the model is successfully entered, the target model is output in the upper right model output window.

4. In the second input box of the upper left input of the tool, enter the slicing reference file.

5. The target model slicing algorithm is executed by pressing the slicing start button at the bottom of the input unit. If the algorithm is successful, only the targets related to the change in the top right output are displayed in blue.