Re: SDL-News: SDL and temporal logic


Subject: Re: SDL-News: SDL and temporal logic
From: Susanne Graf (Susanne.Graf#imag.fr)
Date: Sun Dec 17 2000 - 15:58:48 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 Susanne Graf <Susanne.Graf#imag.fr> to sdlnews -----

Hi,

We have a tool, called IF toolbox
 ( see http://www-verimag.imag.fr/~async/IF/ for the toolbox and
        http://www-verimag.imag.fr/~async/ to know who we are )
which allows to do different type of verifications of SDL specifications. For the
moment it works on a API of the ObjectGeode SDL tool of Telelogic.

The tool-set allows verification of properties expressed as formulas of the
mu-calculus and has shorthands for the usual CTL operators.
Another type of verification which is possible with our tool consists in comparing
the SDL specification modulo bisimulation or simulation with an automaton describing
the property to be verified. This is more expressive than LTL model-checking.

We have many years of experience in using temporal logics as a property language,
and my opinion on their usefulness is the following:
  - temporal logics are very difficult to use for a non expert, and even for
experts. My personal experience is that very often if a system does not satisfy a
somewhat complicated formula, it is the formula and not the system which is false.
Some years ago we implemented a set of macros for the most common properties, which
solved a part of the problem.
  - moreover, the "simpler" logics, like CTL or LTL are not powerful enough to
express all useful properties
  - a relative comfortable way to express properties is by means of automata
labelled by communications between the system and the environment, but also within
the system itself and to compare this automaton -- on the fly or after construction
of the stategraph -- with the behavior of the system.

Susanne Graf
  ----------------------------------------------------------------------
Susanne Graf | tel : (+33) (0)4 76 63 48 52
VERIMAG | fax : (+33) (0)4 76 63 48 50
2, avenue de la Vignate | http://www-verimag.imag.fr/~graf/
F - 38610 Gieres | e-mail: Susanne.Graf#imag.fr
  ----------------------------------------------------------------------

>
> 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 Pedro Merino <pedro#lcc.uma.es> to sdlnews -----
>
> Dear Colleagues,
>
> I am working in the verification of temporal logic properties against
> SDL systems. The idea is to support LTL as a complementary property
> language to MSC.
>
> I know that the AT&T SDLvalid tool support LTL verification. But can
> anybody give me information about other SDL tools supporting temporal
> logic ?
>
> Regards
> Pedro Merino
> --
>
> ---------------------------------------------------------------------------
>
> Pedro Merino Gómez
>
> Universidad de Málaga,

--

--End text from Susanne Graf <Susanne.Graf#imag.fr> 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:49 GMT