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


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).

RSS cloud
Jump to:

List of formal method techniques

1 of 124 articles shown, currently no other people reading this forum.
From: Arran S.
Date: Wed 13th May 2020, 4:27pm


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)



"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

Related articles

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

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