VDM Method

OK, so what is this thing all about?

VDM you mean?

That's why we're here, yeah.

Right. Well, do you know what VDM stands for: the Vienna Development Method?

Something to do with Austria? LOL, okay I have some idea, it's something to do with formal development?

That's right. It was originally developed at the IBM Laboratories in Vienna in the 1970s. It's a way to formally specify computer systems.

Sounds ancient.

I suppose so, yes. But remember the 'C' language came out around then too. Some things stand the test of time. Besides, the theory that underpins VDM is still sound. And it's quite easy to learn and use.

Ah, right. So I could learn about formal specifications with VDM and then move on to something else?

Yes, most of the principles you'll use with VDM apply to other formalisms.

Formalisms?

Ways of developing formal specifications and analysing them, so that usually means a language plus the tools and methods to use it.

Okay, I see. So lots of places teach VDM because it's a good place to start?

I don't know about lots, but it's definitely used for teaching at Aarhus University in Denmark and Newcastle in the UK. There are others.

So if I understand this, I can use VDM to write a specification of a system in a special language?

Yes. You can choose one of three dialects of VDM.

Dialects?

Different forms of the same underlying language. The basic dialect is called VDM-SL; there is an object-oriented extension to it called VDM++; and there is a real time extension of that, called VDM-RT.

Okay, so I write a specification in one of these dialects. But then what do I do with it? I mean, why would I bother?

So it turns out that one of the hardest parts of designing and building a software system is deciding what it should do, as opposed to how it should do it.

That's... quite subtle: what it does, rather than how it does it. Can you explain a bit more?

Think about something very simple like a square root function. The "what it does" would say that the output, when squared, is the same as the input. But the "how it does it" might be a description of Newton's method, or Halley's method, say.

But you're saying that the "what it does" aspect is more difficult than people think?

Sometimes. The problem is that aspects of the "what" are often considered obvious by the people setting requirements, so they don't actually specify them.

A square root seems pretty obvious to me.

Right, because it's just a button on a calculator. Everyone knows what they are. But a square root could produce two results remember, one positive and one negative. And if the input isn't positive, we need to be able to handle imaginary numbers. Did you think of that?

Hmm, good point. I assumed you were talking about positive roots of positive inputs. So you're saying that it's worth spending time to specify all this stuff in detail? Is that really true?

It depends. If your application isn't performing safety critical tasks, or the consequences of it being flawed are pretty minimal, perhaps not. But systems that are used by millions of people might be worth formally specifying, just because of the impact of being wrong.

But the apps on my phone are used by millions of people. These days, if an app has a bug, an update will come out pretty soon to fix it. It's just not that critical, surely?

Right, but what about the software that actually distributes those updates? If that goes wrong, millions of phones could be bricked. So that's pretty critical.

Ah... yeah. But even so, isn't formal specification going to be a lot of effort?

Well, the first thing to understand is that your formal specification will be a LOT smaller than the final system that you write your programs in.

So it must be condensed somehow, or not cover everything?

Yes. We call it an abstract model: it describes the important aspects of your system, but not every little detail.

Still not seeing why that helps though?

Well, by writing down how you intend something to work, you are forced to think carefully about what you really mean. Our square root function can be specified as taking positive inputs and producing positive roots, say. Then the tools will help to check that what you say is consistent and precise, and ultimately allow you to run test simulations of the final system.

Before it's written?

Yes, ideally. Sometimes you might write models in parallel with the development, or to help unpick something that has been developed. But ideally you want to produce the model first.

Doesn't that just slow a project down? Time is money, after all.

It's time well spent. If you stumble into a development without understanding something fundamental about what you need to do, there is a good chance that you will have to throw away a lot of code. If that happens late in a project, it can be very expensive. Formal modelling gives you confidence that you are building something that does what you want, without any nasty surprises.

That sounds too good to be true!

You can still get things wrong, or spend too much time modelling. It's not foolproof. But it's a technique that can help, especially if the cost of faults in your system is large. It also means you can show your system to the people who will ultimately use it early.

But we haven't written it yet?

Yes, that's the point. So rather than wasting lots of time writing something the end user doesn't want, you can show them your understanding early in the project and let them try it out - in an abstract way, of course.

But end users wouldn't understand all this formal stuff, surely?

Of course. But the tools allow you to wrap the formal model in an animation of some sort. So end users can experiment with the proposed system in a friendly way without having to understand the formal notation.

Hmm. Okay, so give me an example of what I could do with VDM and how that helps me?

Well, in general, most systems move from state to state as they receive "input". That input could be API calls from somewhere, or users physically pressing control buttons, or a web server receiving requests over a network and so on. Agreed?

Okay, yes.

And typically, moving from state to state should produce changes that can be described. So if you remove a user account record, it should no longer be present in the database; or if you add something to a basket, the basket will contain the correct new item afterwards; or if you press a button to eject from a plane, the ejection mechanism should engage. Yes?

Yes, I suppose so.

And you may also be able to find things that are always true in the system. Perhaps the sum of the entries in a basket must always match the total line, or perhaps when a plane is on the ground, the undercarriage is always lowered. So if you can find a way to push the system into a state where these things are not true, there is a serious problem.

Like raising the undercarriage when you're parked on the runway...

That's a serious problem, yes.

So all these things are encoded somehow in the specification?

Yes.

And I think I can see that these are "what it does" aspects rather than "how it does it".

Good, yes. These are describing things that the system must always do, or must never do. That is "what" not "how", and sometimes, obvious "what" aspects are overlooked by people. You may not explicitly say that you shouldn't be able to raise the undercarriage when on the ground, because it's obvious. Why would you do that? It's crazy. But a computer system will just do what it's told, crazy or not.

So somehow we can use the formal specification to show that the actions of the system will never break these rules?

Yes, in principle at least. So we can run ad-hoc simulations of specific scenarios, or we can generate thousands of scenarios, or we can use a proof assistant to show that every conceivable scenario will meet the constraints in the specification.

In principle?

The more certain you want to be, the more work it involves. But all of it is based on the fact that we have a formal specification of what the system is supposed to do and not do. Without that, you just have some requirements, and they are often vague or ambiguous.

I see. So when you start implementing this for real, you know that it works. At least as far as the abstract model - you can still have coding errors, presumably?

Oh yes, unless you generate code directly from the formal model, though that only works for very low level parts of a system.

So this must make quite a difference to the way that a software development project operates? I mean, there must be different stages, different processes? How does that work?

Yes, you would do things differently. It mainly affects the start of the project, where the modelling takes place. There's a whole presentation about the process here.

Interesting. So if I wanted to learn how to write my own VDM specifications, can you help?

I'd be happy to give you some pointers, but that's really too complicated for a short discussion. The Wikipedia VDM page is a good start, and there are some good books on the subject here.

OK, thanks, I'll look at that later. So I think I understand what a VDM model is for. Now, what does the VDMJ tool do with VDM models?

Right, good question! That's a different conversation.