Faculty of Engineering and Mathematical Sciences 
Not logged in (login)

help5501

This forum is provided to promote discussion amongst students enrolled in CITS5501 Software Testing and Quality Assurance.

Before posting a question here, you might like to (1) search the forum for previous posts asking the same question, and (2) read the article How To Ask Questions The Smart Way .
And please keep the discussion civil (as required by UWA's Computer Use Policy, #9).
 

Options:
RSS cloud
Jump to:

List of formal method techniques

3 of 124 articles shown, currently no other people reading this forum.
photo
From: David S.
Date: Wed 13th May, 3:13pm
Actions: 
        Login-to-reply

 

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

photo
From: Arran S.
Date: Wed 13th May, 4:20pm
Actions: 
        Login-to-reply

 

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 
de-tainting process.

# Model-based systems

- We haven't yet seen fleshed-out 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 proof-based 
techniques under the hood - I think there are also a few that make use of model-checking - 
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

photo
From: Arran S.
Date: Wed 13th May, 4:27pm
Actions: 
        Login-to-reply

 

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 semi-automated 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 model-based systems and proof-based systems, but the boundary between "type 
system" and "proof system" is especially fuzzy.


[1] Idris: https://www.idris-lang.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 
> de-tainting process.
> 
> # Model-based systems
> 
> - We haven't yet seen fleshed-out 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 proof-based 
> techniques under the hood - I think there are also a few that make use of model-checking - 
> 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
This Page


Program written by: [email protected]
Feedback welcome
Last modified:  3:57pm Aug 06 2020