A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

Pages: **1**

**Beth****Member**- Registered: 2012-03-19
- Posts: 11

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??

Offline

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....

Offline

**Beth****Member**- Registered: 2012-03-19
- Posts: 11

Thanx alot, will do that.

Offline

Pages: **1**