Subject: Re: RE : RE : SDL-News: Difference between simulation and validation inTau sdt
From: Susanne Graf (Susanne.Graf#imag.fr)
Date: Tue Dec 09 2003 - 11:08:01 GMT
Become an SDL Forum Society member <http://www.sdl-forum.org/Society/members.htm>
The originator of this message is responsible for its content.
-----From Susanne Graf <Susanne.Graf#imag.fr> to sdlnews -----
Dear Kim and Mikkel,
yes Daniel is right. I do not know well the TAU tool but it should be quite
close to the ObjectGeode tool. In exhaustive model generation, NOW will always
be zero in your model at the moments you test it. If you want to see an effect
then you should start a local timer when you send a signal, and check if it has
expired when it comes back. Time stamping, as you use it in this model, does not
work well.
Obviously, if there can be several messages "on the way" you need several timers
(e.g. you can generate process for each message). Also your physical medium is
such that communication times are queued: the transmission time of any messages
is added to the transmission times of all the messages in the que at the arrival
time of the message. This might or might not be intended, it's just a remark.
What you can do alternativel, is to use the SDL2IF translator and use the IF
verification tool (which is based on timed automata similar as Uppaal, but it
does also have communication via asynchronous signals, process creation,... in
fact it is quite close to SDL (see http://www-verimag.imag.fr/~async/IF/ for
more details). As your model is very small you have two options: either use the
translator (but you might need an ObjectGeode licence or rewrite the model, If
is really a very simple language, close to textual SDL).
Susanne Graf
VINCENT Daniel FTRD/DTL/LAN wrote:
> Become an SDL Forum Society member <http://www.sdl-forum.org/Society/members.htm>
> The originator of this message is responsible for its content.
> -----From "VINCENT Daniel FTRD/DTL/LAN" <daniel.vincent#rd.francetelecom.com> to sdlnews -----
>
> I don't say it is a state explosion problem. I say "to avoid state explosion problems, some tools have just choosen to avoid progression of NOW" for exhaustive exploration, and this because NOW is part of the state vector, and time passing makes it possible to have an infinite number of states.
>
>
>
> -----Message d'origine-----
> De : Kim Bendtsen [mailto:klbe00#control.auc.dk]
> Envoyé : mardi 9 décembre 2003 10:22
> À : VINCENT Daniel FTRD/DTL/LAN
> Cc : Jens Grabowski; sdl-news#sdl-forum.org
> Objet : Re: RE : SDL-news: Difference between simulation and validation inTau sdt
>
>
> Hi
>
> We dont think it is a state explosion problem, the total number of states we get when validating is below 200 states all depending on the options set in the validator. We have previous hit 5 million states when validating another protocol (simple_protocol is an extraction of the same problem in the our original protocol). Our plan at the moment is to experiment with non-deterministic choices instead of basing the paths on the now variable. We think that this is a poor approximation but may be necessary (at least until we are enlightened otherwise). Also we are considering UppAal eventhough this is not as descriptive for protocols as SDL is but we think the time concept works.
>
> We would still appreciate any help that anybody may have off course
>
>
> Thanks for the answers
> Kim and Mikkel
>
>
>
>>Due to state explosion problems, maybe the Tau validator that you use
>>does not allow the variable NOW to progress when performing exhaustive
>>validation (or it is always reset to 0). Whereas NOW is allowed to
>>progress during interactive or random simulation.
>>
>>Atleast, this is the way the tool ObjectGeode is working, and I guess
>>that Tau took the same decision regarding time progression.
>>
>>When time progression is important, you have the following options:
>> - replace your "time related" decisions by non deterministic decisions (but what to do with timestamps ???)
>> - perform "guided" random simulation
>>
>>These problems of time progression were addressed in the IST INTERVAL
>>project http://www-interval.imag.fr, and a prototype using clocks and
>>time constraints was built, but the results were never integrated in a
>>commercial SDL version.
>>
>>Daniel Vincent
>>France Telecom R&D
>>
>>-----Message d'origine-----
>>De : Kim Led Bendtsen [mailto:klbe00#control.auc.dk]
>>Envoyé : lundi 8 décembre 2003 16:30
>>À : Jens Grabowski
>>Cc : sdl-news#sdl-forum.org
>>Objet : Re: SDL-news: Difference between simulation and validation in Tau sdt
>>
>>
>>Become an SDL Forum Society member
>><http://www.sdl-forum.org/Society/members.htm>
>>The originator of this message is responsible for its content. -----From Kim Led Bendtsen <klbe00#control.auc.dk> to sdlnews -----
>>
>>Thanks for the answer. We have already tried to change the symbol time
>>from zero to undefined and set priorities without any luck. We have
>>uploaded a tar.gz file with the sdl files for Tau4.5 and printed a
>>html version of the system if anybody has the time. This is a very
>>simple protocol. The problem is in the sender process with the
>>decision concerning the 'inPacket!ttl > now'. The false state cannot
>>be reached in the Validator (we know that ttl is used diffrently in
>>IP.. :) )
>>
>>tar.gz file:
>>http://www.control.auc.dk/~03gr938b/sdl/simple_protocol.tar.gz
>>printed html:
>>http://www.control.auc.dk/~03gr938b/sdl/sdl.html
>>
>>Best Regards
>>
>>Kim & Mikkel
>>
>>
>>>if the Validator-principles has not changed in the last 2 years your
>>>problem might be related to the settings of the validator.
>>>
>>>In order to face the problem of state space exploration the
>>>Validator
>>>allows you to drive the state space exploration by using a set of
>>>options, e.g., queue length, handling of time (which might be the
>>>problem in your case) etc. In the past, our validation problems where
>>>mainly related to a special set of options that allows you to
>>>influence the evaluation order of concurrently enabled events by using
>>>priorities. For example, by giving a high priority to system internal
>>>events you can specify something like a reasonable environment, which
>>>waits until the SDL system is in a stable state (i.e., a state where
>>>it waits for the next signal from the environment) before it issues a
>>>new signal.
>>>
>>>The problem that you describe looks like as if the path to be
>>>verified
>>>is not in the set of paths that are explored due to the Validator
>>>settings. You have to play around with these settings (especially with
>>>the settings related to the handling of time).
>>>
>>>Hope this helps.
>>>
>>>Regards
>>>Jens
>>>
>>>
>>>
>>>
>>>Kim Led Bendtsen wrote:
>>>
>>>
>>>>Become an SDL Forum Society member
>>>><http://www.sdl-forum.org/Society/members.htm>
>>>>The originator of this message is responsible for its content.
>>>>-----From Kim Led Bendtsen <klbe00#control.auc.dk> to sdlnews -----
>>>>
>>>>Hi,
>>>>
>>>>We are a group trying to validate a protocol, but are facing a
>>>>problem. We have three blocks in our system a sender, a receiver and
>>>>a physical medium. The sender stamps 'now+packetLifeTime' in the
>>>>packet before transmitting the packet, the physical medium delays
>>>>the packet with one of two possible durations in both directions.
>>>>And the receiver just returns the packet back to the sender.
>>>>When using the simulator we can choose different paths in the simulation
>>>>and have a packet arrive late or in due time. We use the same system in
>>>>the validator and this will show less than 100% coverage and indicate a
>>>>state that is not possible, even though we can simulate and get to
>>>>the state.
>>>>The path that cannot be taken in the validation is after a decision where
>>>>the packet time is compared to 'now'. The semantics are -
>>>>packet!packetLifeTime > now. Decision 1: true, Decision 2: else. Where
>>>>true is never taken.
>>>>
>>>>We have tried to take the MSC from the simulation and verify it in
>>>>the validation, also without luck.
>>>>
>>>>Hope somebody can help
>>>>
>>>>Regards
>>>>
>>>>Kim & Megel
>>>>--End text from Kim Led Bendtsen <klbe00#control.auc.dk> to
>>>>sdlnews
>>>>--- For extra SDL Forum Society benefits join at
>>>><http://www.sdl-forum.org/Society/members.htm>
>>>>For help, email "majordomo#sdl-forum.org" with the body of your email as:
>>>> help
>>>>or (iff this does not answer your question) email: owner-sdlnews#sdl-forum.org
>>>
>>>--
>>>======================================================================
>>>Prof. Dr. Jens Grabowski
>>>Institute for Informatics phone: +49 551 39 14690
>>>University of Goettingen fax: +49 551 39 14415
>>>Lotzestrasse 16-18
>>>DE-37083 Göttingen mailto:grabowski#cs.uni-goettingen.de
>>>(Germany) http://www.swe.informatik.uni-goettingen.de
>>>======================================================================
>>>
>>>
>>
>>--
>> Kim Led Bendtsen
>>--End text from Kim Led Bendtsen <klbe00#control.auc.dk> to sdlnews
>>--- For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm>
>>For help, email "majordomo#sdl-forum.org" with the body of your email as:
>> help
>>or (iff this does not answer your question) email: owner-sdlnews#sdl-forum.org
>
>
>
> --End text from "VINCENT Daniel FTRD/DTL/LAN" <daniel.vincent#rd.francetelecom.com> to sdlnews ---
> For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm>
> For help, email "majordomo#sdl-forum.org" with the body of your email as:
> help
> or (iff this does not answer your question) email: owner-sdlnews#sdl-forum.org
-- ------------------------------------------------------------------------ Susanne Graf | tel : (+33) (0)4 56 52 03 52 VERIMAG | fax : (+33) (0)4 56 52 03 44 2, avenue de Vignate | http://www-verimag.imag.fr/~graf/ F - 38610 Gieres | e-mail: Susanne.Graf#imag.fr --------------------------------------------------------------------------End text from Susanne Graf <Susanne.Graf#imag.fr> to sdlnews --- For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm>
This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT