🚀 go-pugleaf

In article <1992Dec28.064433.14965@cucs5.cs.cuhk.hk>, mklai@ie.cuhk.hk (Edmund M
K Lai) writes:
|> I am looking for ISO protocols of any layer that has already been formally
|> specified in one of the major formal specification languages such as
|> LOTOS and ESTELLE.  So far I have only been able to locate simple data
|> link layer protocols with formal specifications.
|> 

Both Transport and Session Standards have been specified in LOTOS:

@TechReport{ISO10023,
  Author="ISO",
  Title="Information Processing Systems --- Open Systems Interconnection ---
        Formal Description of {ISO} 8072 in {LOTOS}",
  Type=TR, Number=10023,
  Institution="ISO/IEC, Geneva", Month=jul, Year=1992}

@TechReport{ISO10024,
  Author="ISO",
  Title="Information Processing Systems --- Open Systems Interconnection ---
        Formal Description of {ISO} 8073 (Classes 0,1,2,3) in {LOTOS}",
  Type=TR, Number=10024,
  Institution="ISO/IEC, Geneva", Month=jul, Year=1992}


@TechReport{ISO9572,
  Author="ISO/IEC",
  Title="Information technology - Open Systems Interconnection -
        {LOTOS} description of the session protocol",
  Type=TR, Number=9572,
  Institution="ISO/IEC, Geneva", Year=1989 }

@TechReport{ISO9571,
  Author="ISO/IEC",
  Title="Information technology - Open Systems Interconnection -
        {LOTOS} description of the session service",
  Type=TR, Number=9571,
  Institution="ISO/IEC, Geneva", Year=1989 }


-- 
    ___             Harro Kremer                    <kremer@cs.utwente.nl>
 __/   \__________
|  \___/          | Univ. of Twente,   Dept. Computer Science,  TIOS-group
|___     __   ___ | P.O. Box 217,   NL-7500 AE  Enschede,  The Netherlands
| |  |  /  \ (__  |                 tel: +31 53 89 3703 fax: +31 53 333815
| |  |  \__/ ___) | 
|                 | Freedom's just another word for nothing left to loose.
|_________________|                  - Kris Kristofferson & Janis Joplin -

Remember that the formal language specifications of such protocolos as
Transport are advisory.  The formal specification remains the natural
language document, with all its ambiguities.

A compromise position may be to look at the abstract test suites,
written in TTCN, as a "more formal" specification which actually
will be used.  I recognize TTCN is an informal language and a cumbersome
one, but it does have somewhat more formalism than an English-language
specificatin.

In article <C0C1FG.AL9@world.std.com>, hcb@world.std.com (Howard C Berkowitz)
writes:
|> Remember that the formal language specifications of such protocolos as
|> Transport are advisory.  The formal specification remains the natural
			        ^^^^^^
	What interpretation are you using here? Shouldn't this be "official"

|> language document, with all its ambiguities.

|> A compromise position may be to look at the abstract test suites,
|> written in TTCN, as a "more formal" specification which actually
|> will be used.  I recognize TTCN is an informal language and a cumbersome
|> one, but it does have somewhat more formalism than an English-language
|> specificatin.

[ Flames omitted ]
-- 
     ___            Harro Kremer                  <kremer@cs.utwente.nl>
 ___/   \_______
|   \___/       | Univ. of Twente,   Dept. Computer Science,  TIOS-group
| ___    _   __ | P.O. Box 217,   NL-7500 AE  Enschede,  The Netherlands
|  |  | / \ (_  |                 tel: +31 53 89 3703 fax: +31 53 333815
|  |  | \_/ __) | 
|_______________| Freedom's just another word for nothing left to loose.
                                   - Kris Kristofferson & Janis Joplin -

There are several "large" OSI LOTOS specs published as technical reports
by ISO.

ISO 10023 Transport service in LOTOS

I do not know the numbers of the specs in LOTOS of Transport protocol, Session
protocol, session service and network service, but they are there.

Furthermore, in an ESPRIT project we developed several specs of 
ISDN  L3, an ISDN application (small email facility in ISDN phone),
Transaction processing specs (ACSE, CCR, TP).

Regards

-- 
    ___
 __/   \__________  Jeroen van de Lagemaat    <lagemaat@cs.utwente.nl>
|  \___/          |         
|___     __   ___ | University of Twente     
| |  |  /  \ (__  | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217  NL-7500 AE Enschede  The Netherlands
|_________________| tel. +31 53 893684              tfx. +31 53 333815

                    Humour, you're making me laugh.
                                    - Herman Finkers, Dutch comedian -