Benchmark

Dependancies

You need to have these versions or above

• Ocaml 4.13.1
• dune 3.15.0
• opam 2.1.2
• Download the SAG tool from https://github.com/gnelissen/np-schedulability-analysis.git
• Download UPPAAL 5.1.0 or a later version under free academic licence here https://uppaal.org/downloads/

Systems generation

Compilation

• In order to compile the source code for the system generation, use this command :

./exec.sh build

• To clean the workspace use :

./exec.sh clean

• To remove every thing from system_generation/uppaal_files, system_generation/sag_files and system_generation/system_files use :

./exec.sh clear

Execution

• After the compilation, a file named generate will be created in the workspace.
• You can use it to generate our systems by executing :

./generate nb_sys sys_type priority factor distribution utilization test

Where :

• nb_sys : Is the number of system that will be generated.
• sys_type : Is the type of system that will be generated, they can be :
  • Based on both core1 and core2 of waters by mixing all the periods : waters
    • Note that : By choosing this options the systems will be generated by pairs, where System_i will be the core1 and System_i+1 will be the core2 from i = 1,
      both of them will have the same utilization.
  • Same as the previous option, but for this one the tasks : Angle-sync and Taks_1000ms are separated : waters_bis
  • Based on the core1 of WATERS : waters1
  • Based on the core2 of WATERS : waters2
  • Based on the evaluation used in SAG's paper waters_sag
  • Based on an arbitrary distribution of acets, factors and runnable distribution rnd_sys1
  • Based on a random runnable distribution with no acets and no factors rnd_sys2.
    • Note that : The arguments factor and distribution are not affecting the system generate
• priority : Is the type of priority that will be applyed to the set of tasks in a given system, it can be :
  • Randomized : random
  • Rate-Monotonic : rate_monotonic
• factor : Is the method that will be used to generate de wcet factors, it can be :
  • Randomized : random
  • Fixed by keeping the original factors provided in Kramer's paper: fixed
• distribution : Is the method that will be used to distribute the runnables among the tasks, it can be :
  • Randomized : random
  • Fixed by keeping the original distribution in Waters : fixed
• utilization : Is the utilization of all the generated systems.
• test : Is the scheduability test to apply on the systems, it can be :
  • The test proposed in the paper "compositional verification of embedded real-time systems", Journal of Systems Architecture 2023 : test1

OutPut

• generate will create systems and translate them into the adequate input format wich is :
• .rt and .sol in system_generation/uppaal_files for UPPAAL. Note that : it will also generate the queries to verify in a .q format.
• .csv in system_generation/sag_files for SAG.
• .sy in system_generation/system_files in order to get informations about the generated systems.

Translation

• After the compilation, a file named translate will be created in the workspace.
• You can use it to translate a file in the .sy format into the adequate input files for SAG and UPPAAL by executing :

./translate < path_to_fic.sy test

Where :

• fic.sy : Must be a file in the .sy fomrat
• test : Is the scheduability test to apply on the systems, it can be :
  • The test proposed in the paper "compositional verification of embedded real-time systems", Journal of Systems Architecture 2023 : test1

Waters

• To parse the WATERS challenge and get .sy files, you can run

./parse_waters.sh

You can then use translate to get the input files. The frequency used in the parsing is 400MHz, you can switch it to 300MHz if needed.

Benchmarking

• In order to run the benchmark, please make sure that all the dependancies are compiled and ready for usage.
• Once done, run :

./benchmark -h

In order to get all the available options for the benchmak, by defaut :

• The wcrt's are not verifyed.
• The scheduability test is not applyed
• The systems will be based on the core1 of WATERS.
• Tasks priorities are are randomized.
• The wcet factors are fixed.
• The number of generated system is 100.
• The time limit for scheduability analysis is 3600 seconds.

Analysis

• If you want to verify the generated systems using UPPAAL or SAG, you can run respectivly :

./analyse_uppaal.sh

or

./analyse_sag.sh