[comp.protocols.iso] Formal Sprecification in OSI

satam@jambo.ecs.umass.edu (Kirtikumar Satam) (10/11/90)

Few days back I requested information about Estelle, LOTOS and SDL. I
received many replies. Due to these responses, I managed to get some
start on understanding the FDT. I would like to thank all those who have
replied and I am posting a summery of resposes which might help
continuing the discussion and bringing new related topics.
So, here it goes. (Note: There were more replies than those given below.
I have chosen only few to avoid duplication of information. I sincerely
thank all the person whose replies are not included here.)
-----------------------------------------------------
REPLY 1:
From: gram@uctcs.uucp (Graham Wheeler)
Keywords: FDT, Estelle and LOTOS.
Reply-To: gram@staff.UUCP (Graham Wheeler)
Organization: Dept. of Computer Science, University of Cape Town

Estelle (Extended State Transition Language) is a Pascal superset allowing
asynchronous concurrent execution of FSM-based processes communicating via
message passing. It is an implementation-oriented FDT.

Lotos is based on Petri-nets, as far as I can recall. It is much more
`academic' than Estelle.

I heard (second-hand) that Dave Parnas said (at the 2nd International
Conference on FDT's in Canada late last year) that Lotos was popular 
because it had a lot of scope for making little extensions and modifications
and getting publications as a result. Real protocol developers use Estelle
(if they use any FDT).

-----------------------------------------------------
REPLY 2:
From: peter@riovmsc.iinus1.ibm.com
Subject: ISO FDTs

Satam,

Some very basic references are

Bolognesi, T. ane Brinksma, E., 'Introduction to the ISO Specification
Language LOTOS,' Computer Networks and ISDN Networks vol. 14, no. 1 (1987),
pp. 25-59

Budkowski, T. and Dembinski, P. 'An Introduction to Estelle: A Specification
Language for Distributed Systems,' Computer Networks and ISDN Systems vol 14,
no. 1 (1987) pp. 3-23

Belina, F. and Hogrefe, D., 'The CCITT-Specification and Description
Language SDL,' Computer Networks and ISDN Systems vol. 16, no. 4 (1988),
pp. 311-341.

SDL and Estelle are based on extended finite state machine techniques.
A specification divides the behaviour to be specified into subblocks
connected by channels and writes FSMs to describe each subblock.  Subblocks
and channels may be further refined by dividing them in turn.

SDL has been used for many years and exists in graphic and a textual forms.
It is *not* a candidate for ISO standardization, although it is a CCITT
recommendation (I don't have the number).

Estelle is basically an extension to Pascal and is perhaps the easiest for
a programmer to get a handle on, since most of it is very similar to
procedural programming languages.  It is an ISO standard by now.

LOTOS is based on temporal ordering of behaviour (not to be confused with
temporal logic).  Processes synchronize their activities by exchanging
data at interaction points which may be hidden or visible.
LOTOS has nice formal properties which make it good for proving the
equivalence of external behaviors of specifications, so one can show
that a protocol specification satisifies a service definition, for example.
To understand these properties, or to understand LOTOS at all, requires a
good deal of background work to get a grip on the mathematics.  LOTOS is
an ISO standard.


Peter Lonergan
IBM Brazil Rio Scientific Center
peter@riovmsc.iinus1.ibm.com
---------------------------------------------------------
REPLY 3:
From: Richard Tenney <rlt%mote.cs.umb.edu@RELAY.CS.NET>
Subject: Estelle, LOTOS, and SDL
Status: RO

    Your query was forwarded from Alex McKenzie to me.  I was the
editor for IS9074 (Estelle) and remain the "maintenance editor" for
Estelle.  In addition, I am a contributer to ISO/IEC PDTR 10167,
called "GUIDELINES for the APPLICATION of Estelle, LOTOS, and SDL".
This is a "Proposed Draft Technical Report" that is wending its way
through the ISO heirarachy toward becoming a Technical Report. Its
editor is Ken Turner, whose e-mail address is
    "kjt%compsci.stirling.ac.uk%nss.cs.ucl.ac.uk@relay.cs.net" 
(at least this is what works for me).  You may be able to get a copy
through ANSI (it is a fairly large document, over 300 pages).  The
Guidelines document is intended to help people resolve the very
questions you raise by showing some protocols and services specified
in all three techniques you ask about.
    There are Estelle and LOTOS tools (translators, simulators,
intelligent editors, etc.) that have been developed.  You can start by
contacting, say, Paul Amer at the University of Delaware
("amer@louie.udel.edu") and asking him about tools.  There are also
LOTOS tools, which perhaps Peter van Eyk ("pve@cs.utwente.nl") can
fill you in about.
    - Richard Tenney
---------------------------------------------------------
Note: I received a whole-hearted respose from Univ. Of Delaware about
the various tools developed by them. Interested parties can contact
("amer@louie.udel.edu") or Darren New ("new@ee.udel.edu").


------------------------------------------------------------------------------
Kirtikumar Ghanashyam Satam
INTERNET : satam@jambo.ecs.umass.edu
BITNET : satam@umaecs.bitnet
HOME : #68, Colonial Village, Amherst, MA 01002. TEL: 413-253-0954.
SCHOOL : #114, Marcus Hall, Dept. of ECE, UMASS, Amherst, MA 01002.
------------------------------------------------------------------------------