This tool verifies a specification in form of a Property Specificiation Pattern (PSP) against runtime data and assists in refining parameters interactively.
The project can be set up locally either with Docker or the Angular CLI. To get a local copy up and running follow these simple steps.
To run the project using Docker follow these steps.
- Clone the repository and navigate to its root folder
git clone https://github.com/Cambio-Project/transient-behavior-requirement-refiner.git cd transient-behavior-requirement-refiner - Build the containers
docker compose up
- Navigate to
http://localhost:8080/.
For development purposes run a local dev server using the Angular CLI.
- Install Angular CLI
npm install -g @angular/cli
- Clone the repository and navigate to its root folder
git clone https://github.com/Cambio-Project/transient-behavior-requirement-refiner.git cd transient-behavior-requirement-refiner - Install NPM packages
npm install
- Run a local development server
ng serve
- Navigate to
http://localhost:4200/. The application will automatically reload if you change any of the source files.
The tool offers three data sources: Demo, File Upload, and Prometheus.
To quickly explore the tool, three sets of demo runtime data are included. To check them out, set the file source to "Demo" and select one of the demo files.
To analyze your own runtime data, set the file soure to "Upload". Currently, only .csv files are supported in which each column contains a metric and each row represents a time unit. You can find examples for compatible files in the src/assets/csv folder.
Select "Prometheus" as the file source to fetch data from a Prometheus database. Follow these steps to set up a connection and query the database.
If you have your own Prometheus instance running, skip the first step.
- Download Prometheus
https://prometheus.io/download/and check this guidehttps://prometheus.io/docs/prometheus/latest/getting_started/. - Enter the Database URL under "Prometheus Connection URL".
- If the database is password protected, check "Provide Credentials" and enter the username and password.
- Press "Connect".
- Choose a start time, end time, and a step size.
- Choose metrics from the selection list OR activate "Custom Query" and enter your own PromQL query.
- Press "Query".
The following table shows the time for validating and time refinement with no solution (worst case). Validation scales well up to 50000 samples, time refinement up to 10000 samples.
| samples | validation | time-refinement |
|---|---|---|
| 10 | <0.1s | ~0.1s |
| 100 | <0.1s | ~0.4s |
| 1000 | <0.1s | ~34s |
| 10000 | ~0.6s | ~3100s (51 min) |
| 50000 | ~3s | -- |
| 100000 | --------------- out of memory ----------------------- | -- |
To give perspective, for validation-only, reasonable intervals for different sampling rates are:
- 50 seconds interval with a 1 millisecond sampling rate. (50000 samples)
- 1 hour interval with a 75 millisecond sampling rate. (46800 samples)
- 1 day of with a 2 seconds sampling rate. (43200 samples)
- 1 week interval with a 10 seconds sampling rate. (60480 samples)
and for time-refinement, reasonable intervals for different sampling rates are:
- 1 second with a 1 millisecond sampling rate. (1000 samples)
- 1 minute with a 75 millisecond sampling rate. (800 samples)
- 1 hour with a 5 seconds sampling rate. (720 samples)
- 1 day with a 1 minute sampling rate. (1440 samples)
After importing data from one of the sources as described under Import Data, go to the step "Select Pattern" and choose a Property Specification Pattern.
- Select Scope.
- Select Category.
- Select Pattern.
The selected pattern is the basis for the following specification.
Each Pattern consists of one or more predicates that can be specified as follows:
- Expand the specification form by clicking on the "Pen" icon.
- Enter an arbitrary name.
- Select a Measurement Source (this is the predicate's underlying metric from the imported runtime data).
- Select a Logic Operator.
- Set a Comparison Value (not applicable for trend operators).
- Repeat these steps for all predicates of the selected PSP.
The graph next to each specification form visualizes the time dependant evaluation of the predicate. Green areas mark intervalls, in which the predicate evaluates to true. Red areas indicate its evaluation to false.
After specifying all predicates, the overall PSP is evaluated. A green box around the specifiaction indicates, that the given specification is satisfied. An unfulfilled requirement is indicated by a red box. The evaluation result is also displayed in the summary graph at the top of this screen.
The specification and its predicates can be refined manually by the user or assissted by the tool.
To manually refine a specification, change a predicate's comparison value and/or operator. Potenial evaluation changes of the predicate and the overall pattern are visualized interactively.
To automatically refine a specification, click the "Gear" icon next to the "Pen" icon of the predicate to be refined. The tool analyzes the predicate and suggests comparison values for which the overall pattern evaluates to true and false. Note: the suggestions are based on the selected operator. Change the operator to get suggestions other operators.