Re: SDL-News: Difference between simulation and validation in Tau sdt


Subject: Re: SDL-News: Difference between simulation and validation in Tau sdt
From: Kim Led Bendtsen (klbe00#control.auc.dk)
Date: Mon Dec 08 2003 - 15:30:11 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 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>



This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT