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

1 of 124 articles shown, currently no other people reading this forum.
photo
From: Arran S.
Date: Wed 13th May 2020, 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

Related articles

List of formal method techniques (all 3) RSS
├─ original   Wed 13th May 2020, 3:13pm, David S.
├─ THIS   Wed 13th May 2020, 4:20pm, Arran S.
└─ reply 2   Wed 13th May 2020, 4:27pm, Arran S.
This Page


Program written by: [email protected]
Feedback welcome
Last modified: 11:27am Sep 21 2020