Supplementary Data for Multiform: Multi-objective Evolution of Requirements Models Constrained by Formal Verification Results

This data set provides supplementary material for the article "Multiform: Multi-objective Evolution of Requirements Models Constrained by Formal Verification Results" (to appear). It contains the following files: experiment-input-models.zip which contains the SML input models for the EBEAS and production cell examples that were used to conduct the experiment experiment-results.tar which contains the computed candidate SML models as well as H2 database files that contain measurements. experiment-results.pdf which summarizes the conducted controlled experiment and results. Input models (example for EBEAS) ebeas.sml contains the actual SML input model to be evolved ebeas.ecore contains the metamodel of the EBEAS example ebeas.xmi contains the object system of the EBEAS example that is used for the SML realizability check ebeas.runconfig contains the runtime configuration for ScenarioTools that binds the SML input model with the object system ebeas.cspec contains the solution space model used by Multiform. Measurements are stored in an H2 database file. To open one of the database files for the EBEAS or production cell examples extract the appropriate zip file to a local folder, navigate to the folder in a terminal, and start H2 with the appropriate database file as follows: java -jar h2-1.4.199.jar -url jdbc:h2:./Statistics A web-based SQL client will open in your browser. H2 cann be obtained free of charge from their homepage. The database schema consists of three simple tables: SMLCANDIDATESTATISTICS contains measurements for each evolved candidate SML model and consists of the following columns: ALGORITHM - one of 'Random', 'NSGA2', 'tabu-75-intensify' SEED - seed id for which the measurement was taken ITERATION - iteration id during whch the measurement was taken CANDIDATE - unique id of the evaludated candidate SML model SYNTHESISTIME - synthesis time of the evaludated candidate SML model O1_SCENARIOS - objective value for o1 O2_FRAGMENTSRATIO - objective value for o2 O3_ENVFRAGMENTSRATIO - objective value for o3 C1_REALIZABILITY - constraint value for c1 C2_REACHABILITY - constraint value for c1 SMLITERATIONSTATISTICS contains aggregated statistical data for each iteration and consists of the following columns: ALGORITHM - one of 'Random', 'NSGA2', 'tabu-75-intensify' SEED - seed id for which the data was aggregated ITERATION - unique id of this aggregated iteration data ITERATIONSUCCESSRATE - achieved success rate in this iteration ACCUMULATEDSUCCESSRATE - achieved aggregated success reate until this iteration ACCUMULATEDHYPERVOLUMEINDICATOR - achieved hypervolume until this iteration NUMITERATIONPARETOEQUIVALENTCANDIDATES - number of pareto-equivalent candidate SML models in this iteration NUMACCUMULATEDPARETOEQUIVALENTCANDIDATES - number of pareto-equivalent candidate SML models until this iteration NUMITERATIONPARETODOMINANTCANDIDATES - number of pareto-dominant candidate SML models in this iteration NUMACCUMULATEDPARETODOMINANTCANDIDATES - number of pareto-dominant candidate SML models until this iteration ITERATIONSYNTHESISTIME - total synthesis time of this iteration ACCUMULATEDSYNTHESISTIME - accumulated total synthesis time until this iteration SMLSEEDSTATISTICS contains aggregated statistical data for each seed and consists of the following columns: ALGORITHM - one of 'Random', 'NSGA2', 'tabu-75-intensify' SEED - unique id of this aggregated seed data SUCCESSRATE- achieved success rate in this seed HYPERVOLUMEINDICATOR - achieved hypervolume in this seed NUMPARETOEQUIVALENTCANDIDATES - number of pareto-equivalent candidate SML models in this seed NUMPARETODOMINANTCANDIDATES - number of pareto-dominant candidate SML models in this seed TOTALSYNTHESISTIME - total synthesis time of this seed Please note: the database files contain data for algorithms 'tabu-50-intensify' and 'tabu-25-intensify' representing evaluation runs with different Tabu search configurations. However, these still need to be analyzed and experiment-results.pdf refers to 'tabu-75-intensify' only.