The Course Exam Management Case Study (RE03 results)

The Course-Exam Management Case Study (RE03 results)

In the Specifying and Analyzing Early Requirements: Some Experimental Results, a course management case study is used to test the performance and the scalability of the T-Tool. Here you can find the suite that we have used to run the tests and the results of the experiments.

Remarks

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

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] 14.2sec / 38Mb	Consistent[7] 2025sec / 63Mb	Consistent[4] 93.2sec / 96Mb	Undecided M.O.	Consistent[4] 1688sec / 375Mb	Undecided M.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]
9.4sec / 29Mb
Valid[3]
1786sec / 64Mb
Valid[3]
55.7sec / 77Mb
Undecided
T.O.
Valid[3]
860sec / 295Mb
Undecided
M.O.

POSS_2
[P2]
Valid[3]
9.3sec / 29Mb
Valid[3]
1719sec / 63Mb
Valid[3]
55.6sec / 77Mb
Undecided
T.O.
Valid[3]
842sec / 295Mb
Undecided
M.O.

POSS_3
[P3]
Valid[4]
14.2sec / 38Mb
Valid[5]
1979sec / 64Mb
Valid[4]
94.9sec / 96Mb
Undecided
T.O.
Valid[4]
1629sec / 375Mb
Undecided
M.O.

POSS_4

Valid[3]
9.5sec / 30Mb
Valid[5]
1928sec / 64Mb
Valid[3]
56.1sec / 77Mb
Undecided
T.O.
Valid[3]
704sec / 293Mb
Undecided
M.O.

POSS_5

Valid[4]
14.1sec / 38Mb
Valid[5]
1902sec / 64Mb
Valid[4]
90.1sec / 96Mb
Undecided
T.O.
Valid[4]
1512sec / 371Mb
Undecided
M.O.

POSS_6

Undecided[10]
4.0sec / 25Mb
Invalid
1435sec / 64Mb
Valid[3]
56.0sec / 77Mb
Undecided
T.O.
Valid[3]
850sec / 296Mb
Undecided
M.O.

POSS_7

Undecided[10]
3.7sec / 25Mb
Invalid
1357sec / 64Mb
Valid[2]
36.8sec / 60Mb
Undecided
T.O.
Valid[2]
559sec / 226Mb
Undecided
M.O.

POSS_8

Undecided[10]
3.8sec / 25Mb
Invalid
1320sec / 64Mb
Valid[3]
56.6sec / 77Mb
Undecided
T.O.
Valid[3]
887sec / 292Mb
Undecided
M.O.

POSS_9

Valid[3]
9.8sec / 30Mb
Valid[5]
2094sec / 64Mb
Valid[3]
56.3sec / 77Mb
Undecided
T.O.
Valid[3]
974sec / 293Mb
Undecided
M.O.

POSS_10

Undecided[10]
110.5sec / 84Mb
Invalid
1297sec / 64Mb
Valid[4]
89.7sec / 96Mb
Undecided
T.O.
Valid[4]
1483sec / 370Mb
Undecided
M.O.

POSS_11

Valid[4]
13.9sec / 38Mb
Valid[5]
2325sec / 64Mb
Valid[4]
89.6sec / 96Mb
Undecided
T.O.
Valid[4]
1457sec / 377Mb
Undecided
M.O.

POSS_12
[P4]
Undecided[10]
104.9sec / 84Mb
Invalid
1626sec / 64Mb
Undecided[10]
2143sec / 237Mb
Undecided
T.O.
Undecided[4]
T.O.
Undecided
M.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] 112sec / 84Mb	Valid 1501sec / 64Mb	NoBug[9] T.O.	Undecided T.O.	NoBug[4] T.O.	Undecided M.O.
ASSE_2	NoBug[10] 109sec / 84Mb	Valid 1474sec / 64Mb	NoBug[10] 2292sec / 238Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.
ASSE_3	NoBug[10] 111sec / 84Mb	Valid 1525sec / 64Mb	NoBug[10] 1925sec / 239Mb	Undecided T.O.	Invalid[3] 895sec / 294Mb	Undecided M.O.
ASSE_4 [A2]	NoBug[10] 111sec / 84Mb	Valid 1295sec / 64Mb	Invalid[3] 57.6sec / 77Mb	Undecided T.O.	Invalid[3] 2520sec / 296Mb	Undecided M.O.
ASSE_5 [A3]	NoBug[10] 107sec / 83Mb	Valid 2110sec / 64Mb	NoBug[10] 2837sec / 234Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.
ASSE_6	NoBug[10] 3.8sec / 25Mb	Valid 1299sec / 64Mb	NoBug[10] 1126sec / 236Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.
ASSE_7 [A1]	NoBug[10] 100sec / 83Mb	Valid 1298sec / 64Mb	NoBug[10] 1086sec / 237Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.
ASSE_8	NoBug[10] 105sec / 84Mb	Valid 1312sec / 64Mb	NoBug[10] 2374sec / 237Mb	Undecided T.O.	NoBug[4] T.O.	Undecided M.O.
ASSE_9	NoBug[10] 112sec / 84Mb	Valid 1300sec / 64Mb	NoBug[10] 2062sec / 236Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.
ASSE_10 [A4]	NoBug[10] 114sec / 83Mb	Valid 1297sec / 64Mb	NoBug[9] T.O.	Undecided T.O.	NoBug[4] T.O.	Undecided M.O.
ASSE_11	NoBug[10] 104sec / 83Mb	Valid 1432sec / 64Mb	NoBug[10] 1084sec / 235Mb	Undecided T.O.	NoBug[6] T.O.	Undecided M.O.
ASSE_12	NoBug[10] 113sec / 83Mb	Valid 1951sec / 65Mb	NoBug[10] 1952sec / 235Mb	Undecided T.O.	NoBug[5] T.O.	Undecided M.O.

ASSERTION CHECKS (REDUCED MODELS)
	1 instance	1 1/2 instances	2 instances
	BDD-based	BDD-based	BDD-based
ASSE_1	Valid 0.7sec / 2.2Mb	Valid 57.1sec / 29Mb	Valid 1747sec / 150Mb
ASSE_2	Valid 28.9sec / 9.3Mb	Valid 999sec / 63Mb	Undecided T.O.
ASSE_3	Valid 13.7sec / 4.6Mb	Valid 365sec / 65Mb	Undecided T.O.
ASSE_4 [A2]	Valid 18.8sec / 4.8Mb	Invalid[4] 99.2sec / 18Mb	Undecide T.O.
ASSE_5 [A3]	Valid 2.8sec / 2.8Mb	Valid 168sec / 67Mb	Valid 2538sec / 436Mb
ASSE_6	Valid 0.4sec / 2.1Mb	Valid 2.8sec / 3.0Mb	Valid 5.7sec / 3.7Mb
ASSE_7 [A1]	Valid 0.4sec / 2.1Mb	Valid 2.5sec / 3.1Mb	Valid 7.7sec / 5.2Mb
ASSE_8	Valid 1.6sec / 2.6Mb	Valid 136sec / 33Mb	Undecided T.O.
ASSE_9	Valid 1.9sec / 2.4Mb	Valid 19.9sec / 10Mb	Valid 416sec / 68Mb
ASSE_10 [A4]	Valid 3.4sec / 2.9Mb	Valid 117sec / 14Mb	Undecided T.O.
ASSE_11	Valid 0.3sec / 1.9Mb	Valid 0.6sec / 2.2Mb	Valid 1.0sec / 2.7Mb
ASSE_12	Valid 0.5sec / 2.1Mb	Valid 6.9sec / 7.7Mb	Valid 15.3sec / 17Mb

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] 9.4sec / 29Mb	Valid[3] 1786sec / 64Mb	Valid[3] 55.7sec / 77Mb	Undecided T.O.	Valid[3] 860sec / 295Mb	Undecided M.O.
POSS_2 [P2]	Valid[3] 9.3sec / 29Mb	Valid[3] 1719sec / 63Mb	Valid[3] 55.6sec / 77Mb	Undecided T.O.	Valid[3] 842sec / 295Mb	Undecided M.O.
POSS_3 [P3]	Valid[4] 14.2sec / 38Mb	Valid[5] 1979sec / 64Mb	Valid[4] 94.9sec / 96Mb	Undecided T.O.	Valid[4] 1629sec / 375Mb	Undecided M.O.
POSS_4	Valid[3] 9.5sec / 30Mb	Valid[5] 1928sec / 64Mb	Valid[3] 56.1sec / 77Mb	Undecided T.O.	Valid[3] 704sec / 293Mb	Undecided M.O.
POSS_5	Valid[4] 14.1sec / 38Mb	Valid[5] 1902sec / 64Mb	Valid[4] 90.1sec / 96Mb	Undecided T.O.	Valid[4] 1512sec / 371Mb	Undecided M.O.
POSS_6	Undecided[10] 4.0sec / 25Mb	Invalid 1435sec / 64Mb	Valid[3] 56.0sec / 77Mb	Undecided T.O.	Valid[3] 850sec / 296Mb	Undecided M.O.
POSS_7	Undecided[10] 3.7sec / 25Mb	Invalid 1357sec / 64Mb	Valid[2] 36.8sec / 60Mb	Undecided T.O.	Valid[2] 559sec / 226Mb	Undecided M.O.
POSS_8	Undecided[10] 3.8sec / 25Mb	Invalid 1320sec / 64Mb	Valid[3] 56.6sec / 77Mb	Undecided T.O.	Valid[3] 887sec / 292Mb	Undecided M.O.
POSS_9	Valid[3] 9.8sec / 30Mb	Valid[5] 2094sec / 64Mb	Valid[3] 56.3sec / 77Mb	Undecided T.O.	Valid[3] 974sec / 293Mb	Undecided M.O.
POSS_10	Undecided[10] 110.5sec / 84Mb	Invalid 1297sec / 64Mb	Valid[4] 89.7sec / 96Mb	Undecided T.O.	Valid[4] 1483sec / 370Mb	Undecided M.O.
POSS_11	Valid[4] 13.9sec / 38Mb	Valid[5] 2325sec / 64Mb	Valid[4] 89.6sec / 96Mb	Undecided T.O.	Valid[4] 1457sec / 377Mb	Undecided M.O.
POSS_12 [P4]	Undecided[10] 104.9sec / 84Mb	Invalid 1626sec / 64Mb	Undecided[10] 2143sec / 237Mb	Undecided T.O.	Undecided[4] T.O.	Undecided M.O.