Extractor

Extractor

Specstractor is the implementation of the specification-extraction framework originally presented in Ackermann2010 and elaborated on in Schulze2017. The Extractor implements an iterative test -> infer -> instrument -> retest cycle to extract specifications in the form of system invariants from automatically generated test data using data-mining techniques.

The resulting invariants can be analyzed in the [Insight] tool.

The Extractor implements the workflow illustrated in the image below:

1. Generate Test Data: Test data is automatically generated from system models using the Reactis automated coverage testing tool. Reactis actively strives to cover large portions of the systems behavior by targeting different structural coverage metrics, including decision coverage and modified condition/decision coverage (MC/DC).
2. Infer Invariants: Invariants are inferred in the form of association rules, which take the form of implications whose left-hand sides (LHSs) refer to inputs and internal variables and whose right-hand sides (RHSs) are outputs of the system (e.g. input1=1 & internal1=1 -> output1=1). These outputs may themselves be new values for the internal state variables. The invariants are inferred from the test data generated in the previous step using a modified Frequent Pattern (FP)-Growth algorithm from the Sequential Pattern Mining Framework SPMF.
3. Instrument System: To validate the proposed invariants, the system is instrumented with so-called monitor models that represent the proposed invariants. As their name suggests, these monitor models observe the underlying system for any violations of the associated invariants. Reactis provides support for automating this instrumentation processes. (In languages such as C/C++ this is achieved via assert statements.)
4. Retest: The purpose of the retesting phase is to check whether the inferred invariants can be falsified with additional testing. Since the invariants are attached to the models as observers, they are treated as additional coverage objectives by Reactis, which now actively tries to find counterexamples to the proposed invariants. In the process it either disproves invariants, or strengthens the confidence in them by creating additional test data that supports them. In addition to validating existing invariants the additional test data can also uncover new behaviors which lead to invariants that were missed in previous iterations. The test data of all previous iterations is aggregated with the newly created test data and a new set of invariants is inferred in each iteration. If the monitor model detected a counterexample, then the corresponding invariant does not hold true for all test data and is automatically discarded by the data miner. Thus, iterating the approach leads to a more accurate set of invariants.
5. Terminating the Process: The process terminates if there is no change in the set of invariants for N iterations, where N is a parameter set by the user.

Installation Instructions

Prerequisites: * Windows 64bit (Tested on Windows 10) * Reactis 2017 (Tested version 2017.0.1) * Java 8 (Tested on version 8v121)

A 30 day trial license for Reactis can be requested from http://www.reactive-systems.com/ after creating a user account.

The extractor zip file can be downloaded here. After downloading it you can unzip it into a folder of your chosing. The folder structure should look like this:

For licensing reasons we cannot package the Reactis dll files required to execute Reactis from Spectractor. However, the necessary files are included in the Reactis installation. Please copy the file libreactis.dll from ReactisInstallationFolder/lib/api/ to the folder SpecstractorFolder/lib/TestGeneratorDLL/.

Now double click on the Specstractor.jar file to start the Extractor. This should bring up the following screen:

Tutorial

For the Extractor tutorial we will first start by setting up the tutorial system that is in the Specstrator folder. For instructions on how to setup your own system please click here.

System Setup

Please double click on the Specstractor.jar file. After the start screen comes up please click on System Setup. Which will bring up the following screen:

Here click New which will bring up the setup screen below:

On the System Setup screen you have to select the folder that contains the system files, which for our tutorial resides in SpecstractorFolder/tutorial/cruiseSimplified. This is a simplified cruise control system based on the one that comes bundled with Reactis in the folder ReactisInstallationFolder/examples/R2013a/.

Next select the Simulink model of the system SpecstractorFolder/tutorial/cruiseSimplified/tutorial.slx. After selecting the system the Extractor will parse the model file and its inputs and outputs appear in the lists below:

The parser just extracts the input and output blocks of the system. Some of the outputs can be instrumentations of internal states of the system. In this case the output oldActive is such an instrumentation output and has to manually moved to the Inports list by clicking on it and then clicking on the <- red arrow pointing left.

To finish up, select the rsi file SpecstractorFolder/tutorial/cruiseSimplified/tutorial.rsi and the abstraction file SpecstractorFolder/tutorial/cruiseSimplified/abstractions.abs and press the Save button. This will create the file SpecstractorFolder/tutorial/cruiseSimplified/tutorial.rsys which we will use in the next step.

Execute the Extractor

Click the Back button to return to the main screen and then press the Run button which will bring you to a screen with an empty list:

Press the Add button and in the popup window choose the file we created in the System Setup step SpecstractorFolder/tutorial/cruiseSimplified/tutorial.rsys. The screen will change again and the settings for the Extractor execution will appear:

For this example we are supplying manual abstractions and we are therefore using the FP-Growth algorithm. For an example that uses the Range Miner algorithm please press here.

The test generation settings are automatically set to 100/1000/20000 but if you like you can change the number/length of random tests and the number of targeted steps. Before starting the extraction process you have to choose an experiment folder. To do so press the folder button on the top right. Warning: Choose an empty folder since existing files in the folder can be deleted. To start the extraction press the Execute button on the top which will bring up the execution screen.

After the extraction process has finished it will open the folder of the final iteration that contains the Requirements.txt file with the resulting Invariants. To analyze the file either open it in a text editor or load it in the [Insight] tool.