Subject: Re: SDL-News: LTL properties
From: Stefan Leue (sleue#swen.uwaterloo.ca)
Date: Mon Oct 19 1998 - 19:12:43 GMT
The originator of this message is responsible for its content.
-----From Stefan Leue <sleue#swen.uwaterloo.ca> to sdlnews -----
> -----From Philippe.Dhaussy#ensieta.fr (Philippe Dhaussy) to sdlnews -----
>
> 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.,
http://netlib.bell-labs.com/netlib/spin/whatispin.html) 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.
Hope this helps.
Stefan
+------------------------------------------------------------------------+
| Stefan Leue |
|........................................................................|
| Currently visiting (until December 31, 1998): |
|........................................................................|
|Bell Laboratories : Phone : + 1 (908) 582 5495|
|Computing Sciences : Fax : + 1 (908) 582 5857|
|Research Center, Rm 2C-301a: Email : stefan#research.bell-labs.com|
|600-700 Mountain Ave. : WWW : cm.bell-labs.com/cm/cs/who/stefan/|
|Murray Hill, NJ 07974 : : |
|U.S.A. : : |
|........................................................................|
| On leave from: |
|........................................................................|
|Department of Electrical : Phone : + 1 (519) 888 4567 ext. 5313|
| & Computer Engineering : Fax : + 1 (519) 746 3077|
|University of Waterloo : Email : sleue#swen.uwaterloo.ca|
|Waterloo, Ontario N2L 3G1 : : Stefan.Leue#acm.org|
|Canada
+------------------------------------------------------------------------+
-----End text from Stefan Leue <sleue#swen.uwaterloo.ca> 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