Re: [Ufmrg] [EXT] Re: A few questions about UFMRG goals

Hi Joshua,

Thanks for your questions. I think they are very good points. Until this thread, I was under the impression of 1(b) as well.

If the main goal is 1(c), then improving the manuals of tools should be an equally (if not more) important activity. Let's face it: we all know how poorly most (if not all) of these manuals are documented.

> One piece of feedback I get when I ask people why they don't use formal methods is that there is no intermediate level training available.

I don't think this was explicitly clarified before to the volunteers. Some questions in my mind are:

  *   Are the trainers now aware that they are supposed to give intermediate level training and not repeat what they have already presented elsewhere?
  *   Is it still feasible for them to create this intermediate level training within the next 2 months?
  *   Are you certain that you will get enough people in the audience interested in intermediate level training (i.e., well-aware of the basics of the tools)?

Thanks,

Usama

------------------------------------------------------------------------------------------------------------------------------------------
Best Regards,

Muhammad Usama Sardar (M.Sc.)

Research Associate

Technische Universität Dresden

Faculty of Computer Science

Institute of Systems Architecture

Chair of Systems Engineering

Office: APB 3073

Phone: +49 351 463-42048

Email: muhammad_usama.sardar@tu-dresden.de

Website: https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar

------------------------------------------------------------------------------------------------------------------------------------------

________________________________
Von: Ufmrg <ufmrg-bounces@irtf.org> im Auftrag von Jonathan Hoyland <jonathan.hoyland@gmail.com>
Gesendet: Freitag, 8. September 2023 00:27
An: Joshua D Guttman
Cc: Stephen Farrell; ufmrg@ietfa.amsl.com
Betreff: Re: [Ufmrg] [EXT] Re: A few questions about UFMRG goals

Hi Joshua,

One piece of feedback I get when I ask people why they don't use formal methods is that there is no intermediate level training available.

There is documentation for some tools, and sometimes YouTube tutorials for the basics, but unless you work with the tool authors, or people experienced in modelling, there isn't somewhere to learn all the tips and tricks necessary to prove complex things. So people get through a very basic tutorial, and then go look at papers that include huge, complex models, and have no idea how to get between those two places.

The goal of the training is to hopefully build up a set of recorded pieces of training that help people use the tools as they are. By running multiple trainings the hope is to provide a pathway, along with a place you can go and ask questions of experts.

Certainly one of my hopes for this group is that we can provide actionable feedback to tool authors so that they can improve their tools, but starting with the things we can achieve without going outside the group seems like the best way to get started.

Another thing I think we can do fairly immediately is provide guidance on which tools might be most appropriate for which tasks, and thus help work out what work needs to be done to prove the properties we want.

So overall I agree with Stephen's 1c, and mostly 2c. I think the training (along with making the materials available) does make the tool more useable, even though I agree a proper usability study would be even better. I do think there are a number of easy usability improvements to be had in many tools before we need to go for a usability study, so I don't think we're completely unable to proceed on that front.

We are definitely looking for people who have a background in things like user studies to help us make both the training and the group overall a success, so if you have suggestions (or even suggestions of people we can ask) they would be very gratefully received.

Regards,

Jonathan

On Thu, 7 Sept 2023, 23:04 Joshua D Guttman, <guttman@mitre.org<mailto:guttman@mitre.org>> wrote:
I was really impressed by the fast three minute
response, just before the interim mtg a week ago.

But I'm not sure that the reply really gets to the
heart of the matter.

You write:

>    1(c) is fine

in response to:

>>    1.  I'm a little unsure whether the primary
>>    goal is:
>>
>>          (a) To determine whether formal
>>          methods are effectively usable for
>>          IETF-type purposes;
>>
>>          (b) To persuade people that formal
>>          methods are effectively usable for
>>          IETF-type purposes; or
>>
>>          (c) To cause formal methods to become
>>          more effectively usable for IETF-type
>>          purposes.
>>
>>          Of course, a possible response is to
>>          give a blend of more or less of these
>>          three components.  And maybe
>>          additional components?  But what would
>>          be the right characterization?

What makes this a bit askew is the fact that the
most visible activities -- such as the planned
tutorials at the Nov 4 Prague meeting -- really
seem to me closer to 1(b).

I guess the tutorial goal is primarily education.
Since formal methods are in fact very useful, one
expects education to be key to "persuading people
that formal methods are effectively usable for
IETF-type purposes."  ( :- )

And I suspect that persuading and educating may be
a more achievable goal for the UFMRG than actually
causing formal methods to become more effectively
usable.

That requires instead a lot of research, both with
a high level of insight into formal modeling and
proving, and with a bunch of user studies and
appraising the kinds of people who could benefit
from specific kinds of FM.

Would the 4 Nov tutorials even give us any insight
into the latter?

It's conceivable but might require some
coordination and restructuring.

More on question (2) in a separate msg.  I'd be
eager to know what people think about these
aspects of question (1).

        Joshua

On 9/1/23, 12:01, "Stephen Farrell" <stephen.farrell@cs.tcd.ie<mailto:stephen.farrell@cs.tcd.ie>> wrote:

1(c) is fine, 2(c) is closest but not quite right

On 01/09/2023 16:58, Joshua D Guttman wrote:
> May I ask a few questions about the UFMRG goals?
>
> 1.  I'm a little unsure whether the primary goal
>      is:
>
>      (a) To determine whether formal methods are
>          effectively usable for IETF-type purposes;
>
>      (b) To persuade people that formal methods are
>          effectively usable for IETF-type purposes;
>          or
>
>      (c) To cause formal methods to become more
>          effectively usable for IETF-type purposes.
>
>      Of course, a possible response is to give a
>      blend of more or less of these three
>      components.  And maybe additional components?
>      But what would be the right characterization?
>
> 2.  Along another axis, we sometimes have
>      different formal methods that may be useful
>      for different sets of goals (eg establishing
>      that a program respects an inductive invariant
>      vs establishing that a protocol achieves an
>      authentication goal), and maybe also competing
>      formal methods that approach the same goals in
>      different (or similar :- ) ways.
>
>      Do we aim to:
>
>      (a) Identify some methods as suitable for some
>          kinds of goals?
>
>      (b) Grade the usability of some "competing"
>          methods for overlapping goals?
>
>      (c) Identify combinations of methods for
>          purposes that require several kinds of
>          results?
>
>      Again, blends may make sense together.
>
> Thanks!
>
>    Joshua
>
>

--
Ufmrg mailing list
Ufmrg@irtf.org<mailto:Ufmrg@irtf.org>
https://www.irtf.org/mailman/listinfo/ufmrg