List of formal method techniques
3 of 124 articles shown, currently no other people reading this forum.



From: 
David S. 
Date: 
Wed 13th May 2020, 3:13pm 
Actions: 



Hi
Sorry i should have asked this in the workshop but didn't get to watch yesterday's
lecture until just now
For exercise two in the workshop
"Exercise 2
Of the formal method techniques we have considered in class, which might be applied to
the following systems?"
we were meant to reference formal method techniques we have considered in class. I
just wanted to get a clearer picture of what was considered a technique.
We went through program verification as a technique and then at the end of the lecture
discussed there were proof based and model based techniques. My current understanding
is that program verification is an example of a proof based technique. And i know that
it was mentioned in the workshop that 'advanced type based analysis'(?) was an example
of a model based technique. But i'm not sure if i was meant to take any other specific
techniques away from what we've covered so far. Is there a list of techniques
somewhere we're expected to know a bit about?
Kind regards
David

List of formal method techniques


From: 
Arran S. 
Date: 
Wed 13th May 2020, 4:20pm 
Actions: 



Hi David,
I'd say the techniques are:
# Program verification/proofs of correctness
(These are basically the same thing: proving that a program meets its specification.)
 I suppose you could subdivide that, they I didn't say too much about the subdivisions.
 You could say "use of Dafny" is applying a particular formal methods technology...
 As would be the old method of "manually doing Hoare logic".
 But I'd be happy with just "program verification".
# Type systems
 And within these, we mentioned "type systems that enforce unit consistency"
 And at a couple of points in the unit, I've mentioned what are called "type systems for
taint analysis"  these mark input received from users as "tainted" (i.e., potentially
dangerous) and don't allow it to be output (e.g. to a web page) until it has been through a
detainting process.
# Modelbased systems
 We haven't yet seen fleshedout examples of these, but we have mentioned a few of the tasks
they are good at. (Some of them are well suited to analysing state diagrams, for instance.)
In answer to your questions: advanced type systems are distinct enough that most people would
consider them as being in their own class of formal methods. They tend to rely on proofbased
techniques under the hood  I think there are also a few that make use of modelchecking 
but I'd class them as being their own sort of system.
So the above list of three things is probably sufficient for now. Apologies that I didn't
make that clear enough in the slides. I'll take another look at the slides and worksheet, and
add some additional information to the website if I notice anything else that seems lacking.
cheers
Arran
"David Steketee" <21*6*1*[email protected]*u*e*t*u*a*e*u*a*> wrote:
> Hi
>
> Sorry i should have asked this in the workshop but didn't get to watch yesterday's
> lecture until just now
>
> For exercise two in the workshop
> "Exercise 2
> Of the formal method techniques we have considered in class, which might be applied to
> the following systems?"
>
> we were meant to reference formal method techniques we have considered in class. I
> just wanted to get a clearer picture of what was considered a technique.
>
> We went through program verification as a technique and then at the end of the lecture
> discussed there were proof based and model based techniques. My current understanding
> is that program verification is an example of a proof based technique. And i know that
> it was mentioned in the workshop that 'advanced type based analysis'(?) was an example
> of a model based technique. But i'm not sure if i was meant to take any other specific
> techniques away from what we've covered so far. Is there a list of techniques
> somewhere we're expected to know a bit about?
>
> Kind regards
> David

List of formal method techniques


From: 
Arran S. 
Date: 
Wed 13th May 2020, 4:27pm 
Actions: 



Oh  and some people would consider advanced type systems to only be "lightweight formal methods",
or not to be formal methods at all.
But it's a fuzzy dividing line. There are some programming languages whose type system basically
*is* a semiautomated proof system (the language Idris[1] is an example of one these). There are
some proof systems that can also be regarded as programming languages. (The Agda[2] system is an
example of this.)
For our purposes, I'm happy to say that "advanced type systems" are their own sort of formal method,
distinct from both modelbased systems and proofbased systems, but the boundary between "type
system" and "proof system" is especially fuzzy.
[1] Idris: https://www.idrislang.org/
[2] Agda: https://en.wikipedia.org/wiki/Agda_(programming_language)
cheers
Arran
"Arran Stewart" <ar*a*.*t*w*r*@*w*.*d*.*u> wrote:
> Hi David,
>
> I'd say the techniques are:
>
> # Program verification/proofs of correctness
>
> (These are basically the same thing: proving that a program meets its specification.)
>  I suppose you could subdivide that, they I didn't say too much about the subdivisions.
>  You could say "use of Dafny" is applying a particular formal methods technology...
>  As would be the old method of "manually doing Hoare logic".
>  But I'd be happy with just "program verification".
>
> # Type systems
>
>  And within these, we mentioned "type systems that enforce unit consistency"
>  And at a couple of points in the unit, I've mentioned what are called "type systems for
> taint analysis"  these mark input received from users as "tainted" (i.e., potentially
> dangerous) and don't allow it to be output (e.g. to a web page) until it has been through a
> detainting process.
>
> # Modelbased systems
>
>  We haven't yet seen fleshedout examples of these, but we have mentioned a few of the tasks
> they are good at. (Some of them are well suited to analysing state diagrams, for instance.)
>
> In answer to your questions: advanced type systems are distinct enough that most people would
> consider them as being in their own class of formal methods. They tend to rely on proofbased
> techniques under the hood  I think there are also a few that make use of modelchecking 
> but I'd class them as being their own sort of system.
>
> So the above list of three things is probably sufficient for now. Apologies that I didn't
> make that clear enough in the slides. I'll take another look at the slides and worksheet, and
> add some additional information to the website if I notice anything else that seems lacking.
>
> cheers
>
> Arran
>
>
> "David Steketee" <21*6*1*[email protected]*u*e*t*u*a*e*u*a*> wrote:
>
> > Hi
> >
> > Sorry i should have asked this in the workshop but didn't get to watch yesterday's
> > lecture until just now
> >
> > For exercise two in the workshop
> > "Exercise 2
> > Of the formal method techniques we have considered in class, which might be applied to
> > the following systems?"
> >
> > we were meant to reference formal method techniques we have considered in class. I
> > just wanted to get a clearer picture of what was considered a technique.
> >
> > We went through program verification as a technique and then at the end of the lecture
> > discussed there were proof based and model based techniques. My current understanding
> > is that program verification is an example of a proof based technique. And i know that
> > it was mentioned in the workshop that 'advanced type based analysis'(?) was an example
> > of a model based technique. But i'm not sure if i was meant to take any other specific
> > techniques away from what we've covered so far. Is there a list of techniques
> > somewhere we're expected to know a bit about?
> >
> > Kind regards
> > David

