Subject: Specification verification tools

From: "Henning G. Schulzrinne" <[email-masked]>
Date: Wed, 03 Oct 2001 10:33:49 -0400

Recently, the IESG sent a note describing and encouraging the use of
formally verifiable means of protocol specification, in addition to
English prose. To facilitate this effort, I will be setting a resource
web page to provide information on mechanisms and tools. (Unless there
is a formal IETF effort, of course.)

For now, please send me pointers to tools and possible languages or
other suitable means, including, for example, RFC 2234 (ABNF), ASN.1 as
used for LDAP and SNMP, or XML schemas. Note that these tools are meant
for verification, not for code generation.

This is a "freelance" effort, and any statements or listings do not
necessarily reflect official IETF or IESG policy or recommendations.

Thank you.
-- 
Henning Schulzrinne   http://www.cs.columbia.edu/~hgs

---

From: Phil Griffin <[email-masked]>
Date: Wed, 03 Oct 2001 14:45:15 -0400

That note mentioned ASN.1 and several others.

Some language development that might be of interest
that bridges both ASN.1 and XML can be found to
various extents at:

   http://asn1.elibel.tm.fr/en/xml/
   http://www.eetimes.com/story/OEG20010807S0038
   http://www.ddj.com/news/fullstory.cgi?id=4341
   http://xml.coverpages.org/ni2001-02-28-e.html
   http://xml.coverpages.org/xer.html

This ASN.1 XML standards work should be completed
next week at an ASN.1 group meeting in Orlando,
FL, then immediately balloted. I understand that
tools support for this work is slated for fourth
quarter 2001 delivery.

There is a free tools list on the first site
listed, which I believe offers several ASN.1 syntax 
checkers as well as pointers to other free and for
sale tools. Some of these are general, others quite
specialized.

The new ITU-T ASN.1 Project is in the process of
compiling a list of verified ASN.1 modules that 
are being made freely available to anyone at
http://www.itu.int:2001/ITU-T/asn1/database/.

Currently these seem to include only ITU-T 
specifications, but I do not know what their
intended scope may be. An on line base of 
correct IETF ASN.1 modules would certainly be
useful. A note to the web master or contact
might reveal more.

And of course, all of the ASN.1 and SDL standards
are now freely available from the ITU-T web site.
A revision of ASN.1 is currently underway that 
will incorporate all of the TCs and amendments 
into a new 2002 edition.

Phil Griffin

---

From: "Tim Moors" <[email-masked]>
Date: Wed, 3 Oct 2001 14:45:32 -0400

Here are a couple to start with:

Holzmann's book: Design and Validation of Computer Protocols:
http://cm.bell-labs.com/cm/cs/who/gerard/popd.html
http://theory.lcs.mit.edu/~mass/comm.html
http://www.sdl-forum.org/
including the introduction to SDL 88:
http://www.sdl-forum.org/sdl88tutorial/index.html
SDL Integrated Tool Environment:
http://www.informatik.hu-berlin.de/Themen/SITE/
The regular FORTE/PSTV conferences
http://uluru.poly.edu/~tmoors/net/confs.html#forte

Tim Moors
___________________________________
Web: http://uluru.poly.edu/~tmoors/

> -----Original Message-----
> From: [email-masked] [mailto:[email-masked]]On Behalf Of
> Henning G. Schulzrinne
> Sent: Wednesday, October 03, 2001 10:34 AM
> Subject: Specification verification tools
>

---

From: "Francois Menard" <[email-masked]>
Date: Wed, 3 Oct 2001 16:02:36 -0400

Hopefully, the venue of XML in the ASN.1 community will result in more
open source PER runtime objects... 

-=Francois=-

-----Original Message-----
From: [email-masked] [mailto:[email-masked]] On Behalf Of Phil
Griffin
Sent: October 3, 2001 2:45 PM
To: Henning G. Schulzrinne
Cc: [email-masked]
Subject: Re: Specification verification tools

There is a free tools list on the first site
listed, which I believe offers several ASN.1 syntax 
checkers as well as pointers to other free and for
sale tools. Some of these are general, others quite specialized.

Phil Griffin

> other suitable means, including, for example, RFC 2234 (ABNF), ASN.1 
> as used for LDAP and SNMP, or XML schemas. Note that these tools are 
> meant for verification, not for code generation.
>

---

From: "Perry E. Metzger" <[email-masked]>
Date: 03 Oct 2001 16:39:01 -0400

> open source PER runtime objects... 

I can only shudder at the thought at what sort of monster the child of
XML and ASN.1 would be...

--
Perry E. Metzger		[email-masked]
--
NetBSD Development, Support & CDs. http://www.wasabisystems.com/

---

From: Phil Griffin <[email-masked]>
Date: Wed, 03 Oct 2001 20:18:45 -0400

Francois,

Yes, more access to freely available PER tools
would be a help. But even encodings as verbose
as BER and DER tend to compare favorably with
XML Encoding Rules (XER) representations. PER
generally though does better.

Phil Griffin

---

From: Jiri Kuthan <[email-masked]>
Date: Sat, 06 Oct 2001 00:11:55 +0200

http://www.ops.ietf.org/abnf/

--
Jiri Kuthan            http://iptel.org/~jiri