Re: SDL-News: LTL properties

Subject: Re: SDL-News: LTL properties
From: Bernd Grahlmann ( )
Date: Tue Oct 20 1998 - 15:29:08 GMT

The originator of this message is responsible for its content.
-----From (Bernd Grahlmann) to sdlnews -----

Dear Philippe,

> > I am interested to specify temporal properties with LTL or an other
> > temporal logic.
> > Could somebody suggest a tool to compile temporal logic specifications
> > into finite state machines (SDL observers) ?
> > Any pointers are also most welcome.
> I am not sure to what extent this suits your purpose, but the
> Spin/Xspin toolset (c.f.,
> allows you to
> synthesize Buechi automata (there called Promela "never claims") from
> LTL formulae. Note that the properties that you can specify in Xspin's
> LTL property manager are *state* properties of a Promela model, not
> event properties. Hence, you cannot specify constraints on the
> occurrence of communication events directly, this has to be encoded in
> state propositions. There are a few papers in the literature that
> show how Promela relates to SDL, as well how SDL goes together with
> LTL.

Maybe, the following goes a bit further:

The PEP tool supports verification of temporal logic formulae for SDL
specifications. To be precise, (a restricted class, covering however,
e.g., dynamic creation and termination of processes and procedures of)
SDL specifications are automatically compiled into Petri nets.
After this, Petri net simulations may trigger SDL simulations and
temporal logic properties of the SDL specifications may be checked.
This is done in several different ways:
1. We have an interface to the Spin verifier (the Petri nets are transformed
   into PROMELA code, LTL properties are transformed into never claims,
   Spin is used for the verification, an error-trail may be simulated,
   e.g. in the SDL editor).
2. We offer a partial order based model checker which allows you to
   verify a restricted class of CTL formulae. The user may, e.g., ask
   whether there exists an instance of a certain process `Sender',
   such that whenever this instance is in state `wait' while its
   input queue is non-empty, then it may reach a state `send'
   while its variable `X' has value 3:
      EXISTS id IDSET(Sender):
           AG ((Sender[id].state = wait & Sender[id].noqueue > 0)
                 -> (EF (Sender[id].state = send & Sender[id].X = 3 )))
   Such a formula is transparently tranformed into a Petri net formula,
   which is then checked against the Petri net semantics.
   A resulting counter example may again be simulated in the SDL editor.
3. We have an interface to the hardware verification package SMV which
   offers BDD based CTL model checking. This works in almost the same way.

Anyone, who is interested may have a look at our Web-page:
There you can download the tool and find a lot of related papers.

The integration of Spin into PEP is described in:

        AUTHOR = {Bernd Grahlmann and Carola Pohl},
        BOOKTITLE = {{Proceedings of the SPIN'98 Workshop}},
        MONTH = nov,
        TITLE = {{Profiting from Spin in PEP}},
        YEAR = {{1998}},

Hopefully, at the end of this week we will provide an improved transformation
of SDL LTL properties into Petri net LTL properties.

For those who are mainly interested in the integration of SDL into the
PEP tool (the Petri net semantics and the verification possiblities)
I can provide a copy of my (submitted) Ph.D. thesis on demand.

Anyone, who will be in Paris (nex month) for FORTE/PSTV and/or the SPIN Workshop
may contact me for a demo of the PEP tool.

Hope it helps,

Bernd Grahlmann Universit"at Oldenburg Fachbereich Informatik
Telefon (+49) 0441 / 798-3308 Postfach 2503
Telefax (+49) 0441 / 798-2965 D-26111 Oldenburg

-----End text from (Bernd Grahlmann) to sdlnews -----
For help, email "" with the body of your email as:
or (iff this does not answer your question) email:

This archive was generated by hypermail 2a23 : Sun Jun 16 2013 - 10:41:40 GMT