Subject: SDL-News: SDL verification
From: Bernd Grahlmann (bernd#informatik.uni-hildesheim.de )
Date: Tue Aug 11 1998 - 13:13:51 GMT
The originator of this message is responsible for its content.
-----From bernd#informatik.uni-hildesheim.de (Bernd Grahlmann) to sdlnews -----
Dear SDL tool builders and users,
we have recently included SDL support in our verification tool PEP.
Now, I would be interested to compare the verification results with
other tools. One interesting point is the atomicity of SDL state
transitions. According to the Z.100, SDL state transitions are not
atomic. The following example demonstrates the impact:
____________________________________________________________________
system arq;
syntype sigval = Integer
constants 0,1
endsyntype;
signal data(sigval), ack(sigval);
block foo;
signalroute d from client to server with data;
signalroute a from server to client with ack;
process client(1,2);
fpar x sigval;
dcl y sigval;
procedure sendpackage;
start;
output data(x) via d;
return;
endprocedure;
start;
decision parent;
(Null):
task x:=0;
nextstate send;
else:
nextstate send;
enddecision;
state send;
input none;
call sendpackage;
nextstate wait;
state wait;
input ack(y);
decision y=x;
(True):
nextstate send;
else:
again:
create client(y);
decision offspring;
(Null): join again;
else: stop;
enddecision;
enddecision;
endprocess;
process server;
dcl z sigval;
start;
nextstate receive;
state receive;
input data(z);
decision any;
(): output ack(0) to sender;
(): output ack(1) to sender;
enddecision;
nextstate -;
endprocess;
endblock;
endsystem;
____________________________________________________________________
If you follow the Z.100 (and thus allow non-atomic SDL transition) there is
a deadlock:
1. All initialisation and initial process instance creation
steps are performed.
2. The first client instance sends data.
3. The server instance answers with a correct
acknowledgement.
4. The first client instance receives the acknowledgement.
5. The first client instance creates a new (second) client instance.
6. The second client instance sends data.
7. The server instance answers with a correct
acknowledgement.
8. The second client instance receives the acknowledgement.
9. The second client instance tries to create a new (third)
client instance.
This is not possible because this would exceed the maximal number
of allowed client process instances.
Thus, according to the Z.100, Null is returned.
10. In the SDL system, the client process is specified
in such a way that it does not check the return value
(which is stored in the implicit variable Offspring).
Thus, the second client instance terminates.
11. The first client instance terminates.
12. The server process is blocked, waiting for data.
(I agree, that in many cases it makes sense to deviate from the Z.100
regarding this point. Moreover, it is for sure that this blows up
the state space ;-)
My first question is:
Are there any other tools which are able to find this deadlock?
(and how long does it take)
My second question concerns verification of temporal logic properties:
Are there any other tools which are able to verify the following formulae?
(and how long does it take)
EXISTS id IDSET(server): ^(server[id].noqueue>1)
EXISTS id IDSET(client): ^(client[id].noqueue>1)
(^ = possible at some time)
E.g. Is there an instance of the client process such that it is possible that
the input queue of this process instance contains at some point more than
one signal.
FORALL id IDSET(client): ^(client[id].state=send)
FORALL id IDSET(client): ^(client[id].state=wait)
FORALL id IDSET(server): ^(server[id].state=receive)
E.g. Do all the instances of the server process may reach the state receive.
FORALL id IDSET(server): ##(-(server[id].state=LEAVING * server[id].noqueue>0))
FORALL id IDSET(client): ##(-(client[id].state=LEAVING * client[id].noqueue>0))
(## = always)
(- = not)
(* = and)
E.g. Is it for all instances of the client process the case, that the input queue
never contains a signal if this instance has started its termination (which is
non-atomique in our semantics).
##(-(client.noinstances=2 * (FORALL id IDSET(client): (client[id].state=send + client[id].state=wait))))
Is it never possible that two instances of the client process are active
and both of them are in the state send or wait. For instance, the first one in
state send and the second in state wait.
FORALL id IDSET(client): ##^(client[id].state=send)
FORALL id IDSET(client): ##^(client[id].state=wait)
FORALL id IDSET(server): ##^(server[id].state=receive)
May all instances of the client process always (independly from the simulation
steps before) reach the state send.
EXISTS id IDSET(client): ##^(client[id].state=wait) * ##^(client[id].state=INTERNAL)
Is there an instance of the client process such that this instance may always
reach the state wait and may always reach the internal state (during an SDL
state transition).
Thanks for your help,
Bernd
*********************************************************************
Bernd Grahlmann Universit"at Hildesheim
Dipl. Inform. Institut f"ur Informatik
Telefon (+49) 05121 / 883 -760 /-740 Samelsonplatz 1
Telefax (+49) 05121 / 860 475 D-31141 Hildesheim
bernd#informatik.uni-hildesheim.de
*********************************************************************
-----End text from bernd#informatik.uni-hildesheim.de (Bernd Grahlmann) to sdlnews -----
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
This archive was generated by hypermail 2a23 : Sun Jun 16 2013 - 10:41:40 GMT