[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / AG / MCS / SDL / Eval-sdl2if2pml
Printer-friendly
Evaluation of SDL2IF and IF2PML

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
Both tools run on SunOS only. For sdl2if one also requires a Telelogic license key with the license feature SDL_API 1.1.
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"
Now you can compile and execute the model checker as follows:

[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]
Background information about this tool can be found here.

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:

  1. What process of the SDL specification is mapped to what process in PROMELA?
  2. What channel of the SDL specification is mapped to what channel in PROMELA?
  3. How to specify the propery in LTL, never claims or trace assertions?
Questions 1 and 2 can (almost?) be answered algorithmically since both tools, sdl2if and iof2pml somewhat preserver the labellings of the SDL specification. Basically only suffixes are added. The second question however is non-trivial and would at least involve more complicated algorithmics. (Is this even decidable in general?)

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)

Appendix 2: LTL as substitution for trace assertions?

We tried to find out if the trace assertions mentioned above can be replaced by simple LTL formulae. Unfortunately we were not able to find out if that is possible, since there exists quite some literature that gives examples about how the LTL connectives are translated into never claims, but we could not find any, where there is explicitly explained what the universe of the LTL used in SPIN actually is. We do know that boolean expressions, that can be evaluated at a givben state, are allowed as propositions. However we were unable to find out if e.g. message send/receive events can be used either. The latter is necessary to reason about traces.
Valid HTML 4.01 Strict! Valid CSS!