Modelling large models with large integers limit

Beth · 2012-06-07 21:37:18

Hi,
I am in the process of modelling an RSA-based digital signature in SPIN but i got a hitch. The integer limit in SPIN is approximately (2×10^9) but for my model to work as expected, i need to implement at least a limit of approximately (2×10^16) and more .What kind of abstraction would you advice me to apply??

spinroot · 2012-06-09 18:42:14

Often you can verify problems that have very large limits by defining a much smaller version of the problem.
Basically, what you are looking for is what we call the 'smallest sufficient model:' small enough to represent the boundary cases, but not so small that the essence of the problem itself changes.
So you'd want to find a representation of this problem that requires no more than, say a range of 2^8 or so (to pick a very low bound), rather than the real bound which would put a verification with model checking far out of reach....

Beth · 2012-06-10 23:14:42

Thanx alot, will do that.

Spinroot

#1 2012-06-07 21:37:18

Modelling large models with large integers limit

#2 2012-06-09 18:42:14

Re: Modelling large models with large integers limit

#3 2012-06-10 23:14:42

Re: Modelling large models with large integers limit

Board footer