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 the first thing to understand is that your specification will be a LOT smaller than the final system that you write your programs in.

Okay, 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. 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, exactly. 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.

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 somehow we can 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.

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.