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. It has also been taught at the universities in Porto, Dublin, Manchester, London, Kyushu, Aberystwyth and Wisconsin. There are others.

But it's used in industry too? I mean, it's not just for teaching?

Yes, it's used in a variety of industrial projects. For example, the first European validated Ada compiler was developed using VDM. And the semantics of CHILL and Modula-2 were described in their standards using VDM. More recently, the next generation of chip and PIN cards, EMV2, is being modelled in VDM. And it is used in several projects for safety-critical medical devices. There are some more examples on Wikipedia.

Okay. 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?

It's the difference between requirements and design. Perhaps we should really say there can be problems with the communication between the people who know what it should do and the people who know how to do it. The former group are experts in whatever field the software covers; the latter are software engineers who are experts in that field.

But you're saying that the "what it does" aspect is more difficult to describe than you'd 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. Think about a simple function for example, like calculating a square root.

That seems pretty obvious to me.

Right, because it's just a button on a calculator. Everyone knows what they are. But are they really that simple?

Well... yeah?

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. If you're building a sophisticated mathematics package, or working in an engineering field with complex numbers, that could be important.

Okay, you got me: I assumed you were talking about positive roots of positive inputs. But surely it's not worth spending time to specify all this small stuff in detail?

Well, that was just an example to help you see the point. You probably wouldn't specify a maths library like that, but surprisingly often, the assumptions that "customers" and "developers" make are not the same. Sometimes that's harmless or resolved quickly. But not always and the resulting problems can be expensive.

But you wouldn't go to this trouble for every development, surely?

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?

That's true. But what about the software that actually distributes those updates? If that goes wrong, you can't then distribute updates to fix the problem. Millions of phones could be bricked. So that's pretty critical.

Ah... that would be a disaster, yes. But even so, isn't formal specification going to be a lot of effort?

Not necessarily. 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 what something must do precisely, 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 building 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?

Right, but the tools allow you to wrap the formal model in an animation of some sort -- a simple GUI, say. 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 requirements, 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 a plane is 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.

Okay, I see that. But if it's something that experts wouldn't think of, and the developers wouldn't think of it either, how can a formal specification hope to define it? I mean, why would you think of it when specifying formally, if you wouldn't think of it anyway?

That's a fair point. But the idea is that, by elaborating the "what" aspects of the system, these details come out to make it consistent. For example, you can imagine a set of rules for what a plane can and can't do before takeoff, when it's in the air, and when it lands again. There might be limitations on the power level of the engines for example, and certain other systems must be engaged or not when you're on the ground, in the air, or as you come in to land.

And you're saying there might be a rule about the undercarriage?

Well, you would typically specify all the rules, and how these rules change as the plane takes off, and as it lands, because these are important transitions. The engines can use full power as you take off, for example, but not before. At some point after takeoff the undercarriage must be raised, perhaps with a constraint that you must be at a certain minimum altitude and airspeed.

So that will make the specifier wonder why there were no rules about the undercarriage in the earlier phase on the ground. They ask the experts. The experts say, "Well duh, the undercarriage is lowered on the ground." Everyone has a laugh and the model is corrected to say that. But the process of walking through the "what" of the whole system led you to uncover these small details, as part of making it all consistent.

I see. So it's the consistency of the formal model that lets you find things that you wouldn't otherwise think of. And this level of description is definitely all about "what it does". I see that now.

Right! We're not talking about programming here. This is just trying to unambiguously capture the rules about what the system must always do and must never do. It's quite a skilled job and distinct from that of programming. It's closer to requirements engineering, but with a splash of formality.

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, probably written in English, and they are often vague or ambiguous, just like English. You can't test a specification written in a natural language, so you have to trust that everyone has the same understanding of it, that it is complete and unambiguous.

I see. So when you start implementing something formally specified 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. But remember the formal model can act as an 'oracle' for testing the real system, so unlike natural language requirements, the model is active and can be used to verify the implementation, if you follow careful practices.

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, different testing? How does that work?

Yes, you would do things differently. It mainly affects the start of the project, where the requirement 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.