iSpin Tcl/Tk [tcltk] Spin. iSpin , . 2.1 1.
. 2.1. iSpin
:
Edit/View , , , Promela. ( ), ;
Simulate/Replay , , , , ;
Verification , / , ;
Help ;
Swarm Run ;
Save Session/Restore Session ;
Quit .
2.1.1. Edit/View
Edit/View iSpin . 2.2. :
1 , : Open - ; ReOpen - ; Save/Save As - ; Syntax Check - Promela; Redundancy Check - ; Symbol Table - ; Find - ;
. 2.2. Edit/View
2 Promela;
3 ( ) , proctype, init, , (never claims), ;
4 , Syntax Check, Redundancy Check, Symbol Table.
|
|
2.1.2. Simulate/Replay
Simulate/Replay iSpin . 2.3. :
1 ;
. 2.3. Simulate/Replay
2 : , (blocks new messages), , (loses new messages);
3 . , , ;
4 : (Re)Run - / , Stop - , Rewind - , Step Forward/Step Backward - ( , );
5 spin , ;
6 Promela, ;
7 Message Sequence Chart (MSC) [msc];
8 , .
Spin :
1. (Random), (. seed) . .
2. (Interactive). .
3. (Guided, with trail). , , , .trail. .
, , . : (initial steps skipped), (maximum number of steps), (Track Data Values). .
: , , . , Track Data Values. : _ (_): _ = _.
|
|
: _: proc _ (_) . : __: ____ (state _) [ ]. , : 20: proc 5 (node:1) leader0.pml:22 (state 1) [printf('MSC: %d\\n',mynumber)], , 20 5 node 1, printf('MSC: %d\\n',mynumber), 22 leader0.pml. _ , ____ . , , MSC.
( chan Promela) .
2.1.3. Verification
Verification iSpin . 2.4. :
. 2.4. Verification
1 (Safety) (Liveness);
2 (never claims): use claim .
3 ;
4 , : ( depth-first search) ( breadth-first search). ( partial order reduction). report unreachable code ;
5 , : (Show Error Trapping Options) spin (Show Advanced Parameter Settings).
6 (Run), (Stop) (Save Result in);
7 Promela, ;
8 .
( ) . ( safety) : invalid endstates (deadlock) - ( , , init-, : , , end); assertion violations - ( assert ); xr/xs assertions - ( xr ) ( xs ) .
( liveness) : non-progress cycles - ( , progress); acceptance cycles - , accept; enforce weak fairness constraint - ( Spin ).
|
|