A forum for Spin users
You are not logged in.
Pages: 1
Hi,
I have been trying to post a question but this message keeps on popping. What could be the problem??
"An appropriate representation of the requested resource /fluxbb/post.php could not be found on this server.
Additionally, a 404 Not Found error was encountered while trying to use an ErrorDocument to handle the request."
Thanks alot
Hi,
Just a minor clarification. How do you compute the number of states that can be handled by SPIN if i have 1.99GB of memory and a state vector of 1 byte?
Thanks in advance.
Thanx alot, will do that.
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??
Hi again,
Well am working on a 32-bit laptop and i verified my model using -w32 as advised but the same "unreached code" popped up. I moved to a 64-bit laptop later on and used -w33 but the same problem persists from the .pml code(BS process) in my model and onwards. A snippet of the verification run is shown below:
Bit statespace search for:
never claim + (SecrecyProperty)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 940 byte, depth reached 1612, errors: 0
2.7560651e+09 states, stored
8.7938966e+08 states, matched
3.6354548e+09 transitions (= stored+matched)
1.2513312e+08 atomic steps
hash factor: 3.11674 (best if > 100.)
bits set per state: 3 (-k3)
Stats on memory usage (in Megabytes):
2512739.431 equivalent memory usage for states (stored*(State-vector + overh
ead))
1024.000 memory used for hash array (-w33)
0.038 memory used for bit stack
0.343 memory used for DFS stack (-m10000)
1.092 other (proc and chan stacks)
1025.515 total actual memory usage
unreached in proctype BS
ReMT2ndProtocol2.pml:233, state 7, "BSindex_i = 0"
ReMT2ndProtocol2.pml:235, state 11, "BSindex_i = 2"
ReMT2ndProtocol2.pml:236, state 13, "BSindex_i = 3"
ReMT2ndProtocol2.pml:237, state 15, "BSindex_i = 4"
ReMT2ndProtocol2.pml:248, state 50, "Nbs = (Nbs-20)"
ReMT2ndProtocol2.pml:270, state 73, "BSCommit = -(1)"
ReMT2ndProtocol2.pml:276, state 105, "PK_BS = (PK_BS-20)"
ReMT2ndProtocol2.pml:277, state 115, "BSRunning = -(1)"
(8 of 129 states)
unreached in proctype SS
ReMT2ndProtocol2.pml:338, state 25, "SSTSSI = (SSTSSI-20)"
ReMT2ndProtocol2.pml:360, state 47, "SSRunning = -(1)"
ReMT2ndProtocol2.pml:368, state 105, "PN_index = (PN_index-20)"
ReMT2ndProtocol2.pml:369, state 168, "PN_index = (PN_index-20)"
ReMT2ndProtocol2.pml:370, state 203, "PK = (PK-20)"
ReMT2ndProtocol2.pml:377, state 240, "Nss = (Nss-20)"
ReMT2ndProtocol2.pml:409, state 272, "SSCommit = -(1)"
ReMT2ndProtocol2.pml:410, state 278, "SSCommit = 1"
ReMT2ndProtocol2.pml:410, state 280, "SSCommit = -(1)"
ReMT2ndProtocol2.pml:410, state 283, "((0==Legit))"
ReMT2ndProtocol2.pml:410, state 283, "else"
(10 of 288 states)
unreached in proctype Intruder
ReMT2ndProtocol2.pml:572, state 140, "KPK_BS = 1"
ReMT2ndProtocol2.pml:574, state 160, "KSSResult = 1"
ReMT2ndProtocol2.pml:574, state 162, "KBSResult = 1"
ReMT2ndProtocol2.pml:588, state 190, "KSSResult = 1"
ReMT2ndProtocol2.pml:588, state 192, "KBSResult = 1"
(5 of 202 states)
unreached in claim SecrecyProperty
_spin_nvr.tmp:8, state 8, "-end-"
(1 of 8 states)
pan: elapsed time 4.21e+04 seconds
pan: rate 65417.642 states/second
What could the problem be?? can i really trust bitstate hashing since from what i have read, its best when the hash factor is greater than 100??
I also tried to use -w34 and onwards but got the message >> "Segmentation fault (core dumped)", does it mean that -w33 is the limit??
Hi,
In the process of verifying my model(a security protocol), an exhaustive search was infeasible due to limitations in memory. I therefore resorted to using bitstate hashing since it faster and consumes less memory compared to the other optimization techniques currently supported by SPIN. Well, the verification output did not generate an error yet there was a huge list of unreachable code within the model. What does this exactly mean??was this verification effective??
Thanks alot.
I modeled a simple cryptographic protocol, an intruder process and specified secrecy properties to be satisfied by the protocol in LTL. I later verified the model and got a violation to the specification as expected. SPIN automatically generated a trail fail corresponding to the error as shown below. The thing is, what does the numbers separated by the colons mean?? How do i interpret the below trail??
-2:3:-2
-4:-4:-4
1:0:592
2:2:100
3:0:598
Thanks,it worked.
Hi, i just started using iSPIN for the implementation of my project. Quick question, where should i place the Never Claims generated from LTL formulas??? Should it be within a process in my model or outside the process?? any assistance on the above matter will be highly appreciated.
Pages: 1