Subject: RE : RE : SDL-News: Difference between simulation and validation inTau sdt
From: VINCENT Daniel FTRD/DTL/LAN (daniel.vincent#rd.francetelecom.com)
Date: Tue Dec 09 2003 - 09:52:15 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 "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>
This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT