Symbolic Observation Graph-Based Generation of Test Paths

sog-test-paths generates the observable paths from a Petri net model. It also generates the abstract paths.

Requirements

• A C++ compiler (gcc >= 9.3.0).

Use

To compile the tool you have to:

• First, run the make command inside the directory buddy22 in order to build the library used to manipulate Binary Decision Diagrams (BDD).

• Second, run make in the parser directory in order to build the library used to parse Petri net models from net files.

• Third, run the make command in the root directory to generate the executable file StructAnalysis.

-To run this executable on any example, we have to access the main directory and execute the command "./StructAnalysis ./Samples/file.net" for the paper we used the example file Samples/exemple.net.

--- Exemple ------------------------------------------

We treat the exemple of 2 dining philosophers. The figure bellow represents the Petri Net corresponding to 2 philosophers.

*Step1: Extract the set of unobservable transitions using the pattern. For this exemple Unobs={GoEat0, GoLeft0, GoRight0, GoEat1, GoLeft1, GoRight1}.
*Step2: Deduce the set of observable transitions. Obs={Release0, Release1}.
*Step3: Build the SOG (Symbolic Observation Graph) starting from the Petri Net and the set of observable transitions and build the observable paths on the fly. We get the set of observed paths {<Release0>,<Release1>}.
*Step4: Complete the Observable paths by unobservable transitions by making backtracking in each aggregate. The final result for this example is the set of abstract paths (complete paths): {<GoEat0 GoRight0 GoLeft0 Release0>,<GoEat1 GoRight1 GoLeft1 GoEat0 Release1>}

----Experimental result ----------------------------

We have applied our approach to the Dining philosophers problem by varying the number of philosophers each time (2,3...100 philosophers). We evaluate the size of the reachability graph, the number of observed transitions , the number of aggregates found by applying our tool and calculate the execution time for each example. We notice that the size of the reachability graph is increasing exponentially. The results are summarised in the attached table.