Subject: SDL-News: Difference between simulation and validation in Tau sdt
From: Kim Led Bendtsen (klbe00#control.auc.dk)
Date: Mon Dec 08 2003 - 13:18:50 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 -----
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>
This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT