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

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