The Course Exam Management Case Study

The Course-Exam Management Case Study

In the Specifying and Analyzing Early Requirements: Some Experimental Results, a couse management case study is used to test the performance and the scalability of the T-Tool. In this page you will be able to access to the test suite we used to run the tests. Moreover, there are also tables reporting the results of the experiments.

Remarks

The excerpts of FT specification that appear in the paper have been edited for explanatory purposes.

The results reported here are remarkably better than the results reported in the RE03 paper (available here). The improvements are due only to the re-engineering of the T-Tool occurred after the paper acceptance. Further noticeabale improvements can be obtained by fine-tuning the BDD-package to better fit the models resulting from the transaltion of the new versione of the tool. These results have been obtained using the setting for the BDD package that we used in the test suite of the paper.

The test suite
The test suite can be found here. It contains the following directories:

bin/
Contains the executables of the T-Tool (ft2il, il2smv, TNuSMV, ltl2smv).
model_paper/Contains the full FT model and the reduced FT models corresponding to the specification that has been used for the tests in the paper. In order to test the performance of the T-Tool in the case of buggy specifications, some bugs have been kept in this specification.
model_correct/Contains the full FT model and the reduced FT models corresponding to the correct specification.
tests/Contains the scripts for running the different tests. They are test_consistency, test_possibilities, test_assertions, and test_assertions_reduced and generate the data for the 4 tables in the next section. The tests have been set up in order to run on model_paper.
tmp/For temporary files.

The results
As explained in the paper, the tests have been runned on models of different size, namely to the cases of

one instance for each class (1 instance),
two instances for the classes related to the student and one instance for the classes related to the teacher (1 1/2 instances),
two instances for each class (2 instances).

The experiments have been performed using both BDD-based model checking and BMC-based model checking. In the latter case, the bound for the length of the (counter-)examples has been set to 10.

For each experiment we report the result in the first line and the time (in seconds) and memory (in Mb) in the second line. "T.O." means that the experiment has not ended in the time limit (1 hour). "M.O." means that the experiment has exceeded the memory limit (1 Gb). The results have been obtained on an Intel Xeon 700Mh running Linux.

Consistency checks
The following table reports the results of the consistency checks.
Legenda:

Consistent[#n] - The specification is consistent, a witness of length #n has been found.
Inconsistent - The specification is inconsistent.
Undecided - The consistency of the specification has not been decided (due to a T.O. or M.O.).
Undecided[#n] - The consistency of the specification n has not been decided. No withness has been found up to length #n (BMC-based experiments).

CONSISTENY CHECKS
	1 instance		1 1/2 instances		2 instances
	BMC-based	BDD-based	BMC-based	BDD-based	BMC-based	BDD-based
CONSISTENCY	Consistent[4] 4.93sec / 14.7Mb	Consistent[7] 148.7sec / 29.6Mb	Consistent[4] 22.17sec / 45.3Mb	Undecided T.O.	Consistent[4] 178.7sec / 115Mb	Undecided T.O

Possibility checks
The following table reports the results of the possibility checks.
Legenda:

Valid[#n] - The possibility condition is valid, a witness of length #n has been found.
Invalid - The possibility consition is not valid, i.e., it cannot be satisfied by the specification.
Undecided - The validity of the condition has not been decided (due to a T.O. or M.O.).
Undecided[#n] - The validity of the condition has not been decided. No withness has been found up to length #n (BMC-based experiments).

REMARK: The results reported in the paper correspond to the possibilities marked as [P1] - [P4] in the following table.

POSSIBILITY CHECKS

1 instance
1 1/2 instances
2 instances

BMC-based
BDD-based
BMC-based
BDD-based
BMC-based
BDD-based

POSS_1
[P1]
Valid[3]
3.84sec / 11.3Mb
Valid[5]
144.24sec / 29Mb
Valid[3]
12.7sec / 34Mb
Undecided
T.O.
Valid[3]
71.0sec / 85Mb
Undecided
T.O.

POSS_2
[P2]
Valid[3]
3.85sec / 11.3Mb
Valid[5]
144.27sec / 29Mb
Valid[3]
12.57sec / 34Mb
Undecided
T.O.
Valid[3]
71.19sec / 85Mb
Undecided
T.O.

POSS_3
[P3]
Valid[4]
4.90sec / 14.7Mb
Valid[5]
147.14sec / 29Mb
Valid[4]
23.03sec / 45Mb
Undecided
T.O.
Valid[4]
207.76sec / 114Mb
Undecided
T.O.

POSS_4

Valid[3]
3.81sec / 11.3Mb
Valid[5]
145.18sec / 29.6Mb
Valid[3]
12.6sec / 35Mb
Undecided
T.O.
Valid[3]
88.26sec / 87Mb
Undecided
T.O.

POSS_5

Valid[4]
4.9sec /14.7Mb
Valid[5]
145.5sec / 29Mb
Valid[4]
20.82sec / 45Mb
Undecided
T.O.
Valid[4]
138.27sec / 113Mb
Undecided
T.O.

POSS_6

Undecided[10]
2.75sec / 10Mb
Invalid
139.44sec / 29Mb
Valid[3]
12.62sec / 34Mb
Undecided
T.O.
Valid[3]
73.07sec / 85Mb
Undecided
T.O.

POSS_7

Undecided[10]
2.66sec / 10Mb
Invalid
136.36sec / 29Mb
Valid[2]
7.61sec / 25Mb
Undecided
T.O.
Valid[2]
42.91sec / 60.5Mb
Undecided
T.O.

POSS_8

Undecided[10]
2.75sec / 10Mb
Invalid
135.18sec / 29Mb
Valid[3]
12.97sec / 35Mb
Undecided
T.O.
Valid[3]
80.26sec / 86Mb
Undecided
T.O.

POSS_9

Valid[3]
3.89sec / 11.6Mb
Valid[5]
150.60sec / 29Mb
Valid[3]
12.75sec / 34Mb
Undecided
T.O.
Valid[3]
81.95sec / 86Mb
Undecided
T.O.

POSS_10

Undecided[10]
26.9sec / 36Mb
Invalid
136.2sec / 29Mb
Valid[4]
21,42sec / 45Mb
Undecided
T.O.
Valid[4]
147.57sec / 114Mb
Undecided
T.O.

POSS_11

Valid[4]
4.91sec / 14Mb
Valid[5]
150.4sec / 29Mb
Valid[4]
21.67sec / 103Mb
Undecided
T.O.
Valid[4]
156.51sec / 114Mb
Undecided
T.O.

POSS_12
[P4]
Undecided[10]
24.74sec / 36Mb
Invalid
140sec / 29Mb
Undecided[10]
482sec / 113Mb
Undecided
T.O.
Undecided[7]
T.O.
Undecided
T.O.

Assertion checks
The following tables reports the results of the assertion checks for the full model and for the reduced models (see Section 3.3 of the paper).
Legenda:

Valid - The assertion condition is valid, no counter-example has been found.
Invalid[#n] - The assertion consition is not valid, a counter-example of length #n has been found.
Undecided - The validity of the assertion has not been decided (due to a T.O. or M.O.).
NoBug[#n] - No counter-examples have been found up to length #n (BMC-based experiments).

REMARK: The results reported in the paper correspond to the assertions marked as [A1] - [A4] in the following tables.

ASSERTION CHECKS (FULL MODEL)
	1 instance		1 1/2 instances		2 instances
	BMC-based	BDD-based	BMC-based	BDD-based	BMC-based	BDD-based
ASSE_1	NoBug[10] 27.68sec / 36.3Mb	Valid 141.7sec / 29.6Mb	NoBug[10] 2689.60sec / 116Mb	Undecided T.O.	NoBug[5] T.O.	Undecided T.O.
ASSE_2	NoBug[10] 27.14sec / 36.6Mb	Valid 140.6sec / 29.6Mb	NoBug[10] 924.90sec / 115Mb	Undecided T.O.	NoBug[6] T.O.	Undecided T.O.
ASSE_3	Nobug[10] 25.95sec /36.6Mb	Valid 139.6sec / 29.6Mb	NoBug[10] 415.33sec / 116Mb	Undecided T.O.	Invalid[3] 82.24sec / / 87.2Mb	Undecided T.O.
ASSE_4 [A2]	NoBug[10] 29.08sec / 96Mb	Valid 135.8sec / 29.6Mb	Invalid[3] 13.72sec / 34.5Mb	Undecided T.O.	Invalid[3] 120.68sec / 85.6Mb	Undecided M.O.
ASSE_5 [A3]	NoBug[10] 26.04sec / 36Mb	Valid 156.1sec / 29.7Mb	NoBug[10] 456.45sec / 113Mb	Undecided T.O.	NoBug[8] T.O.	Undecided T.O.
ASSE_6	NoBug[10] 3.26sec / 10.2Mb	Valid 145.5sec / 29.6Mb	NoBug[10] 312.08sec / 113Mb	Undecided T.O.	NoBug[10] 2679.57sec / 30.2sec	Undecided M.O.
ASSE_7 [A1]	NoBug[10] 2.65sec / 10.2Mb	Valid 132.52sec / 29.6Mb	NoBug[10] 285.48sec / 113Mb	Undecided T.O.	NoBug[10] 2341.49sec / 30.2Mb	Undecided T.O.
ASSE_8	NoBug[10] 24.56sec / 36Mb	Valid 135.3sec / 29.6Mb	NoBug[10] 430.04sec / 113Mb	Undecided T.O.	NoBug[7] T.O.	Undecided T.O.
ASSE_9	NoBug[10] 26.57sec / 36.1Mb	Valid 135.4sec / 29.6Mb	NoBug[10] 626.87sec / 113.4Mb	Undecided T.O.	NoBug[6] T.O.	Undecided T.O.
ASSE_10 [A4]	NoBug[10] 27.66sec / 36.1Mb	Valid 135.4sec / 29.6Mb	NoBug[10] 2684.32sec / 114Mb	Undecided T.O.	NoBug[4] T.O.	Undecided T.O.
ASSE_11	NoBug[10] 25,24sec / 35.6Mb	Valid 140sec / 29.6Mb	NoBug[10] 266.83sec / 112.7Mb	Undecided T.O.	NoBug[10] 2314sec / 299Mb	Undecided T.O.
ASSE_12	NoBug[10] 26.68sec / 36.4Mb	Valid 151sec / 29.6Mb	NoBug[10] 421.67sec / 112.9Mb	Undecided T.O.	NoBug[7] 2939sec / 300Mb	Undecided T.O.

ASSERTION CHECKS (REDUCED MODELS)
	1 instance	1 1/2 instances	2 instances
	BDD-based	BDD-based	BDD-based
ASSE_1	Valid 0.24sec / 1.8Mb	Valid 5.03sec / 7.6Mb	Valid 848.95sec / 44Mb
ASSE_2	Valid 1.22sec / 2.4Mb	Valid 60.48sec / 31Mb	Undecided T.O.
ASSE_3	Valid 0.48sec / 2.2Mb	Valid 5.82sec / 8.9Mb	Undecided T.O.
ASSE_4 [A2]	Valid 1.15sec / 2.4Mb	Invalid[4] 6.13sec / 3.6Mb	Undecide T.O.
ASSE_5 [A3]	Valid 0.52sec /2.1Mb	Valid 10.26sec / 12Mb	Valid 90.35sec / 43Mb
ASSE_6	Valid 0.22sec / 1.8Mb	Valid 0.24sec / 2.1Mb	Valid 0.92sec / 2.2Mb
ASSE_7 [A1]	Valid 0.22sec / 1.8Mb	Valid 0.28sec / 2.1Mb	Valid 0.67sec / 2.3Mb
ASSE_8	Valid 0.32sec / 2Mb	Valid 5.20sec / 8.1Mb	Valid 371.17sec / 62Mb
ASSE_9	Valid 0.35sec / 2Mb	Valid 3.65sec / 3.2Mb	Valid 169.95sec / 27Mb
ASSE_10 [A4]	Valid 0.52sec / 2Mb	Valid 8.88sec / 5.3Mb	Valid 50.23sec / 17.4Mb
ASSE_11	Valid 0.22sec / 1.8Mb	Valid 0.25sec / 1.9Mb	Valid 0.44sec / 2.2Mb
ASSE_12	Valid 0.23sec / 1.8Mb	Valid 0.67sec / 2.6Mb	Valid 3.01sec / 6Mb

Go back to the Formal Tropos Case Studies list.

POSSIBILITY CHECKS
	1 instance		1 1/2 instances		2 instances
	BMC-based	BDD-based	BMC-based	BDD-based	BMC-based	BDD-based
POSS_1 [P1]	Valid[3] 3.84sec / 11.3Mb	Valid[5] 144.24sec / 29Mb	Valid[3] 12.7sec / 34Mb	Undecided T.O.	Valid[3] 71.0sec / 85Mb	Undecided T.O.
POSS_2 [P2]	Valid[3] 3.85sec / 11.3Mb	Valid[5] 144.27sec / 29Mb	Valid[3] 12.57sec / 34Mb	Undecided T.O.	Valid[3] 71.19sec / 85Mb	Undecided T.O.
POSS_3 [P3]	Valid[4] 4.90sec / 14.7Mb	Valid[5] 147.14sec / 29Mb	Valid[4] 23.03sec / 45Mb	Undecided T.O.	Valid[4] 207.76sec / 114Mb	Undecided T.O.
POSS_4	Valid[3] 3.81sec / 11.3Mb	Valid[5] 145.18sec / 29.6Mb	Valid[3] 12.6sec / 35Mb	Undecided T.O.	Valid[3] 88.26sec / 87Mb	Undecided T.O.
POSS_5	Valid[4] 4.9sec /14.7Mb	Valid[5] 145.5sec / 29Mb	Valid[4] 20.82sec / 45Mb	Undecided T.O.	Valid[4] 138.27sec / 113Mb	Undecided T.O.
POSS_6	Undecided[10] 2.75sec / 10Mb	Invalid 139.44sec / 29Mb	Valid[3] 12.62sec / 34Mb	Undecided T.O.	Valid[3] 73.07sec / 85Mb	Undecided T.O.
POSS_7	Undecided[10] 2.66sec / 10Mb	Invalid 136.36sec / 29Mb	Valid[2] 7.61sec / 25Mb	Undecided T.O.	Valid[2] 42.91sec / 60.5Mb	Undecided T.O.
POSS_8	Undecided[10] 2.75sec / 10Mb	Invalid 135.18sec / 29Mb	Valid[3] 12.97sec / 35Mb	Undecided T.O.	Valid[3] 80.26sec / 86Mb	Undecided T.O.
POSS_9	Valid[3] 3.89sec / 11.6Mb	Valid[5] 150.60sec / 29Mb	Valid[3] 12.75sec / 34Mb	Undecided T.O.	Valid[3] 81.95sec / 86Mb	Undecided T.O.
POSS_10	Undecided[10] 26.9sec / 36Mb	Invalid 136.2sec / 29Mb	Valid[4] 21,42sec / 45Mb	Undecided T.O.	Valid[4] 147.57sec / 114Mb	Undecided T.O.
POSS_11	Valid[4] 4.91sec / 14Mb	Valid[5] 150.4sec / 29Mb	Valid[4] 21.67sec / 103Mb	Undecided T.O.	Valid[4] 156.51sec / 114Mb	Undecided T.O.
POSS_12 [P4]	Undecided[10] 24.74sec / 36Mb	Invalid 140sec / 29Mb	Undecided[10] 482sec / 113Mb	Undecided T.O.	Undecided[7] T.O.	Undecided T.O.