|
|
@ -4,14 +4,14 @@ Its parameters are: |
|
|
|
|
|
|
|
|
N = number of chunks in a file |
|
|
N = number of chunks in a file |
|
|
MAX = maximum number of retransmissions |
|
|
MAX = maximum number of retransmissions |
|
|
TD = the transition delay |
|
|
|
|
|
TIME_OUT = the time the sender waits before timing out |
|
|
|
|
|
|
|
|
|
|
|
TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD) |
|
|
|
|
|
|
|
|
TD = the transition delay |
|
|
|
|
|
TIME_OUT = the time the sender waits before timing out |
|
|
|
|
|
|
|
|
|
|
|
TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD) |
|
|
|
|
|
|
|
|
For more information, see the untimed version: http://www.prismmodelchecker.org/casestudies/brp.php |
|
|
For more information, see the untimed version: http://www.prismmodelchecker.org/casestudies/brp.php |
|
|
|
|
|
|
|
|
The PTA extension is based on that used in [HH09] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The PTA extension is based on that used in [HH09] |
|
|
|
|
|
|
|
|
===================================================================================== |
|
|
===================================================================================== |
|
|
|
|
|
|
|
|
@ -19,8 +19,9 @@ The PTA extension is based on that used in [HH09] |
|
|
L. Helmink, M. Sellink and F Vaandrager |
|
|
L. Helmink, M. Sellink and F Vaandrager |
|
|
Proof checking a data link protocol |
|
|
Proof checking a data link protocol |
|
|
In Proc. Types for Proofs and Programs (TYPES'93), LNCS 806, pp 127-165, Springer-Verlag, 1994 |
|
|
In Proc. Types for Proofs and Programs (TYPES'93), LNCS 806, pp 127-165, Springer-Verlag, 1994 |
|
|
[HH09] |
|
|
|
|
|
A. Hartmanns and H. Hermanns |
|
|
|
|
|
A Modest Approach to Checking Probabilistic Timed Automata |
|
|
|
|
|
Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[HH09] |
|
|
|
|
|
A. Hartmanns and H. Hermanns |
|
|
|
|
|
A Modest Approach to Checking Probabilistic Timed Automata |
|
|
|
|
|
Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009 |
|
|
|
|
|
|