![[Mail]](../../../Images/umschlag.gif)
| Michael Weber | Disclaimer | Last modified: 2004-08-04 12:31 UTC |
![[I2 logo]](../../../Images/i2.gif)
![[RWTH logo]](../../../Images/rwth-rot90.gif)
(Informatik 2)
HomeNewsJobsContactStaffTeachingResearchMOVES SeminarDFG-GK AlgoSynCS ChairsLuFG I2
Evaluation of sdl2if and if2pml by example
Tooling employed
This evaluation was done using:- sdl2if: SDL Application Programming Interfaces V1.1.0 ./sdl2if (c) VERILOG 1997
- if2pml: Current version from download page
For details about what is converted how by both tools, see sdl2if and if2pml.
The test case
The test case was taken from the Telelogic Tau SDL Suite manual. It represents a simple coin tossing game "demon game". The original SDL PR representation can be seen here.Translation from SDL PR to the intermediate format IF (sdl2if)
Firstly the license file needs to be copied to a location accessible by sdl2if and the environment variable LM_LICENSE_FILE needs to be set accordingly. Unless this is done, one will only see the following error message when trying to run sdl2if:Error: No SDL_API 1.1 feature in license file
So when the license file is correctly installed, one is able to use sdl2if for conversion. The input file has to have the ending .pr! Then simply invoke ./sdl2if <myfile>.pr and sdl2if will perform the conversion:
[bash] sdl2if: ./sdl2if demongame
SDL Application Programming Interfaces V1.1.0 ./sdl2if (c) VERILOG 1997
"demongame.pr", (0 information)
"demongame.pr", 0 warning
"demongame.pr", 0 error
[bash] sdl2if:
The resulting file will be labeled <myfile>.if.The result of our test can be seen here. Background information about this tool can be found here.
Translation from intermediate Format IF to PROMELA/(DT)SPIN (if2pml)
As described earlier, PROMELA is the Process Meta Language, the input language for the model checker SPIN. if2pml is capable of translations from IF to PROMELA. Thus, it also allows conversion from SDL to PROMELA employing sdl2if. However, it generates code that is actually intended to be used with DTSPIN, a version of SPIN with discrete time extensions. However, the PROMELA model might also be used with standard SPIN, by providing another header file. To convert the file from above, to PROMELA, simply invoke:./if2pml <myfile>.if
This will generate the file <myfile>.if.pml. In the case, the IF representation was generated by sdl2if there should be no syntax error on that stage. If, however, the IF representation was modified and/or generated otherwise, it might contain such errors and in that case, if2pml will report any errors found at the commandline. Also if2pml generates a log file <myfile>.if.log, whose purpose is unknown to us at the moment (file always empty).
The generated promela code for our example can be seen here.
In order to compile this code using DTSPIN, one just has to copy this header file dtimesdl.h into the working directory and invoke dtspin (read here about how to use standard spin):
dtspin -a <myfile>.if.pml
However, be aware, that DTSPIN on some systems shows the following bug: The file pan.h contains in line 1 the following broken comment definition:
#define Version "Spin Version 3.3.10 -- 15 March 2000
+ Discrete-Time Extension Version 0.1.1 -- 4 April 2000"
This has to be changed to:
#define Version "Spin Version 3.3.10 -- 15 March 2000 + Discrete-Time Extension Version 0.1.1 -- 4 April 2000"
[bash] cc pan.c; ./a.out
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 3.3.10 -- 15 March 2000)
+ Partial Order Reduction
Full statespace search for:
never-claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid endstates +
State-vector 144 byte, depth reached 13, errors: 0
10 states, stored
1 states, matched
11 transitions (= stored+matched)
4 atomic steps
hash conflicts: 0 (resolved)
(max size 2^18 states)
1.493 memory usage (Mbyte)
unreached in proctype __Timers
(0 of 5 states)
unreached in proctype main_0
line 70, state 14, "q_game_0!gameover,_pid"
line 67, state 21, "q_main_0?endgame,sender"
line 67, state 21, "q_main_0?newgame,_"
(2 of 22 states)
unreached in proctype game_0
line 106, state 7, "env!score,_pid,count"
line 111, state 12, "env!lose,_pid,0"
line 120, state 30, "q_game_0?probe,_"
line 120, state 30, "q_game_0?result,_"
line 120, state 30, "q_game_0?gameover,_"
line 120, state 30, "q_game_0?bump,_"
line 137, state 32, "env!score,_pid,count"
line 144, state 39, "env!win,_pid,0"
(5 of 45 states)
unreached in proctype demon_0
(0 of 14 states)
unreached in proctype :init:
(0 of 5 states)
[bash]
Performing the actual verification
In our example we knew about the following specification bug beforehand
which we tried to reveal using the PROMELA model: There may be
situations where the Demon process tries to send a message
over one certain channel, however there is no reciever instantiated yet,
which could recieve this message (the example is taken from the SDT
Manual, chapter 5). In order to validate this misbehaviour, one has to
perform the following manual task:- What process of the SDL specification is mapped to what process in PROMELA?
- What channel of the SDL specification is mapped to what channel in PROMELA?
- How to specify the propery in LTL, never claims or
trace assertions?
In our example we decided for the following trace assertion:
trace {
q_game_0!bump(_);q_game_0?bump(_)
}
Here, q_game_0 is the corresponding channel. By this assertion we claim that it is always true that a send event of a bump message on this channel is some time followed by a recieve event on that channel. Certainly, if this is violated, we capture the above situation where there is no reciever ready to recieve the message. So we do not express the very same propery but rather a somehow equivalent. This trace assertion is simply to be added to the file <myfile>.if.pml. SPIN now reports the following:
[bash] cc pan.c; ./a.out
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan: event_trace error (no matching event) (at depth 13)
pan: wrote demongame.if.pml.trail
(Spin Version 3.3.10 -- 15 March 2000)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
trace assertion +
never-claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid endstates +
State-vector 148 byte, depth reached 12, errors: 1
9 states, stored
0 states, matched
9 transitions (= stored+matched)
4 atomic steps
hash conflicts: 0 (resolved)
(max size 2^18 states)
1.533 memory usage (Mbyte)
[bash]
The resulting trail looks as follows:
[bash] spin -p -t demongame.if.pml
1: proc 1 (:init:) line 188 "demongame.if.pml" (state 1) [(run main_0())]
2: proc 1 (:init:) line 189 "demongame.if.pml" (state 2) [(run game_0())]
3: proc 1 (:init:) line 190 "demongame.if.pml" (state 3) [(run demon_0())]
4: proc 4 (demon_0) line 169 "demongame.if.pml" (state 1) [t.val = (0+1)]
5: proc 3 (game_0) line 97 "demongame.if.pml" (state 1) [count = 0]
6: proc 2 (main_0) line 51 "demongame.if.pml" (state 1) [goto game_off]
7: proc 0 (__Timers) line 32 "dtimesdl.h" (state 1) [(timeout)]
8: proc 4 (demon_0) line 177 "demongame.if.pml" (state 6) [((t.val==0))]
transition failed
9: proc 4 (demon_0) line 179 "demongame.if.pml" (state 8) [q_game_0!bump,_pid]
9: proc 4 (demon_0) line 180 "demongame.if.pml" (state 9) [t.val = (0+1)]
10: proc 3 (game_0) line 114 "demongame.if.pml" (state 15) [q_game_0?bump,sender]
11: proc 0 (__Timers) line 32 "dtimesdl.h" (state 1) [(timeout)]
12: proc 4 (demon_0) line 177 "demongame.if.pml" (state 6) [((t.val==0))]
transition failed
13: proc 4 (demon_0) line 179 "demongame.if.pml" (state 8) [q_game_0!bump,_pid]
13: proc 4 (demon_0) line 180 "demongame.if.pml" (state 9) [t.val = (0+1)]
spin: trail ends after 13 steps
#processes: 5
queue 1 (q_game_0): [bump,4]
13: proc 4 (demon_0) line 175 "demongame.if.pml" (state 13)
13: proc 3 (game_0) line 134 "demongame.if.pml" (state 44)
13: proc 2 (main_0) line 56 "demongame.if.pml" (state 12)
13: proc 1 (:init:) line 192 "demongame.if.pml" (state 5) <valid end state>
13: proc 0 (__Timers) line 32 "dtimesdl.h" (state 2) <valid end state>
5 processes created
[bash]
As one can relatively easily see, the first send event of a bump message (step 9) is answered by a recieve event (step 10), however the second one is not (step 13). This makes the trace assertion fail.
Mapping the trace back to SDL
In general it can be said that the mapping of the SPIN trace back to SDL went better than expected. that is due to the graphical state space explorerof Telelogic Tau, that we could use to reproduce the steps in the PROMELA model in the SDL spec. The major challenge is here the fact, that one step in the SDL model is usually reflected by multiple steps in the PROMELA model. So on the way back one has to interpret multiple PROMELA steps in such a way that it becomes clear, what transition to use in the SDL model. In our case this mapping was somewhat obvious, however considering more complicated models and the possible absence of the Telelogic Tau SDL Suite, we guess that one could have quite some trouble on this mapping step. Anyway in out case the error trail could be fully reproduced in the SDL specification.Conclusion
The conversion of SDL to IF is lossy, thus one loses information during that step. The conversion to PROMELA however is relatively intuitive, since PROMELA provides a richer expressiveness than IF.Anyway, due to the loss of information the model checking approach can neither be complete nor absolutely intuitive. Though the level of automation is high, still manual steps are involved when it comes to the requirements specification. Those specification again entirely reasons about the PROMELA model and about this model only. As a result one hast to manually assert that what is specified is actually appropriate to what one actually seeks to specify and also that, what the model checker tells, is actually correctly interpreted from the SDL point-of-view.
Appendix 1:
Using standard (untimed) Spin (source)
The real time properties of the specifications cannot be expressed in
standard Promela and Spin in a quantitative manner. Consequently, the IF
specifications are actually translated into DT Promela, an extension of
Promela with discrete-time features (timers and operations on
timers). Thus it is very likely that standard Spin will report errors if
the IF (SDL) model involves timing. In some cases one can maintain the
original semantics by redefining the timer macros of the header file.
Dragan Bosnacki e.g. proposes in "Model
checking SDL with SPIN" the following substitution:
#define timer bool
#define set(tmr,val) (tmr=true)
#define reset(tmr) (tmr=false)
#define expire(tmr) (tmr==true)
