This project aims at providing a Coq characterisation for models of timed data-flow reactive systems, a class of embedded systems whose inputs and outputs are always available as signals. Input signals can be seen as data provided by sensors, whereas the output data are provided to system actuators. The Coq characterisation allows for a scalable and single framework for specifying, validating, verifying and testing such systems. For a comprehensive explanation of DFRS models, we refer to:
- Modelling timed reactive systems from natural-language requirements (
link)
analyses: contains the necessary files to reproduce our empirical analyses;run: contains Python scripts to automate the execution of our empirical analyses;src: contains the *.v files related to our characterisation of DFRSs in Coq.
In order to reproduce our empirical analyses, one should perform the following steps:
-
Compile our Coq characterisation of timed data-flow reactive systems (see
link); -
Copy all folders from
analysesto the directory where SRCIROR has been installed; -
Configure the parameters declared in
run.py
# List of examples (possibilities = "vm", "tis" and/or "npp")
examplesToRun = ["vm","tis","npp"]
# List of number of Sample calls for each example
samplesNumber = [1,5,10]
# Number of replications for each Sample call and for each example
replications = 5
# Path to SRCIROR
srcirorPath = "/home/ghpc/Documents/srciror"
- Run the main Python script: python run.py
This script will perform the following tasks:
- generate test cases for the selected examples;
- process the QuickChick output and save test data into *.csv files;
- generate mutants from C reference implementations;
- run all test cases against all mutants;
- collect and summarise empirical data.
The obtained results are summarised in the file all_results.csv.
R code for creating box plots is made available in the directory R.
Dependencies: