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


Subject: Re: SDL-News: Difference between simulation and validation in Tau sdt
From: Jens Grabowski (grabowski#informatik.uni-goettingen.de)
Date: Mon Dec 08 2003 - 14:33:34 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 Jens Grabowski <grabowski#informatik.uni-goettingen.de> to sdlnews -----

Dear Kim,

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
======================================================================

--End text from Jens Grabowski <grabowski#informatik.uni-goettingen.de> 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