[MUSIC]

Welcome at this last lecture of this MOOC.

In this lecture, I will look at hierarchical organization of components

such that we can do intermediate reductions and deal with larger systems.

And I also want to look at the explicit specification of external state spaces,

because that makes the intermediate state spaces even smaller.

We saw this small system in the last lecture.

And this is a typical software architecture pattern where you have

a manager process controlling a number of workers.

If we have a big system,

then these systems often have this particular structure.

So, then we have the worker controlling subworkers, and the subworkers

controlling subdevices of devices and they may even in turn, control subdevices.

If this is our structure, then we can actually use what's called

Compositional State Space Generation and Intermediate Reduction.

So the idea is the following.

We take a subpart, and if we have this particular subpart, so let's isolate it.

Then we can actually generate a state space of this

subpart by first hiding the communication, then generating the state space.

State space may still be substantial, then reducing it.

For instance,

modulo branching bisimulation hopefully getting a small transition system.

And if you have the small transition system,

we can replace the original behavior by this reduced behavior.

And in this way we can work our way and replace all subsystems by

this small behavior and we can actually, recursively do this for parts, so

take this system, and generate a small behavior of this system.

Because if we reduce all the behaviors before connecting them,

that state space in this way remains much smaller than when

we would generate the state space of the whole system.

So, this is a typical way to deal with very complex systems and

generate a system state space for the whole system.

And the guideline is, in this case,

that if we make our systems hierarchical, this works quite well.

So, typically what we do is

we iteratively hide communication of a subpart.

We generate the transition system of that subpart.

We reduce the behavior, and

ultimately we get the behavior of the whole state space.

And if it sufficiently small, we can inspect it or

we can verify modal formulas on it.

There are a few disfunctitures.

The first one is that it only works for hierarchical systems.

If systems have another structure, then this approach

can even fire back in the sense that intermediate

state spaces are much larger than the ultimate state space.

So, if one wants to apply this,

one should avoid such more complex communication structures.

The other observation is that the behavior of systems,

if you combine a number of subparts, often is more complex than one would expect.

And that is due to the fact that if you do not think about the desired

external behavior, you get more or less the external

behavior that's in the subcomponents and that's more or less accidental.

So what one should do is that one should first design the external behavior,

and then adapt the subcomponents such that this external

behavior is actually realized.

And that's an important guideline, and

if you apply it in combination with hierarchical systems allows you to

completely model and verify big systems.

So the idea is you design the behavior of a subsystem,

you then consider the subcomponents that are part of the whole system,

and you adapt and tweak the subcomponents such that the desired and

nice external behavior is actually obtained.

And if you do this at all the layers, you obtain

a system that is not only having nice behavior, but that's generally also much

easier to understand for other people, and with that, much easier to maintain and

this is one of the biggest issues with software these days.

And it's also the case that state space remains much smaller than if you

just take the number of subcomponents and let the external behavior come into being.

So let's just illustrate this with a small example.

I look at a device monitor controller.

Actually, it's inspired by Tanenbaum's third sliding window protocol.

Tannenbaum's third sliding window protocol has an appalling complex

external behavior, but it's a little bit too complex to explain here so

I simply find it somewhat with a device monitor controller.

So, but it illustrates exactly the same phenomenon.

So what we have is a device monitor, and that looks at devices and

observe that they are correct or not, and reports about it.

We have a controller, and the controller has a task that it should report about

the broken devices in sequence.

So it first reports about one, then about two, and then about three, etc.

The controller has a buffer.

The size of the buffer is M, because there are M devices and

it simply can record for every device whether it's broken or not.

And the device monitor simply indicates that

a particular device is broken whenever it detects it to the controller.

So it could be that it first reports that three is broken, then one is broken,

five is broken, two is broken.

And it's now the task of the controller to report that back, so

it will first report that one is broken, then two, then three.

Of course, it will not report that four is broken, so it will skip that and

then report that five is broken.

And that does it with the simple out action and this is a little bit

simplified in the sense that it does not report which device is broken,

it only reports that a device is broken and it will report it in order.

Well the system's slightly more complex, so the user of the system that

receives the out messages can stop the system, and it can again start the system.

And when the system stops, there will not be out messages.

That will only be delivered after the system is started again.

So, how do we specify this?

We simply have the behavior of the controller.

The controller has a buffer, which is used to function from natural

numbers to booleans indicating that a device is broken by true, and

that the device is correct by storing false.

It has this boolean b, and b indicates that the system

is working and can deliver out messages then b is true, or it has been stopped and

in that case b is false and then it's not allowed to deliver messages.

And there is this index i, that's the index of

the next device of which it must be reported that it is out of order.

So, what is the behavior?

Of course, the device monitor can always report that a particular device is broken,

so it can do this broken n action indicating that device n is broken.

And then the controller sets

the position n in the buffer at true.

It can be that the controller wants to report, so

this can be done if b is true because then it is allowed to report, and

the buffer at position i should be true because that indicates that

device i is broken and then it will do this out action.

It will set the buffer at that position to false to indicate that it has

been reported and it will increase its index.

If the device at position i is not broken, so the buffer at position i is false,

then it will simply increase its index and it will not report anything.

It will do this internal tau action.

And then we still have the start and stop actions.

So, if there is nothing to report anymore, and

the controller is allowed to report it can be stopped, and

we will set the variable b to false indicating that it cannot report anymore.

And if it's not allowed to report, it can be restarted and

then this boolean b is set to true.

So this is the behavior of the system.

I think it's pretty straightforward.

And the question is how does the external behavior look of

the combination of these systems?

So we hide broken action,

in line with our previous lectures, we take the buffer size to be small.

Actually, it could have taken it to be 1, but in this case we take it to be 2.

And we get this state space.

And this may surprise you somewhat, so if you look at the details of the state

space, you will find that this is indeed correct and this is reduced modulo

branching bisimulation, but this is not quite what one would expect.

And if you look at increasing buffer sizes,

we see the following namely in the second column,

we see the sizes of the state spaces before reduction.

And we see that these sizes are growing exponentially, and that is what we expect.

This is quite normal but we see that external behavior, so

the behavior after reduction modulo branching bisimulation,

has also an exponential growth.

So, if the buffer size is set to M,

the total state space is already 2,000 states big for

the reduced behavior and that looks quite weird.

So we can ask ourselves, what is actually the behavior that we

desire now that we see that this behavior that came into being is somewhat complex.

And if you start thinking about this then this might be the behavior that we desire,

enabling this if the system is off, it will not report.

If the system is on, it will report.

That certain devices are out of order, and that is what we expect to see.

And now the question is, if we look at this original specification,

why isn't it the case that we get this nice and expected behavior?

And it turns out that the problem is here, we can only stop the system

if we have nothing to report anymore.

So what we could do is that we say we can always stop the system

by hiding this part of the condition.

And what we see is that in that case,

the behavior of the whole system becomes all opposite of this desired behavior.

It used this particular detail in a condition that causes

this enormous and horrendous external behavior.

And what we also see is that this is completely independent

of this buffer size.

The external behavior always reduces to 2.

And what I think is that this shows that by consciously

thinking about how the external behavior should look like,

one can indeed make systems with much nicer external

behavior than that's done these days by many people that

are not aware of the existence of external behavior.

Okay, let's look at an exercise.

So, here we have a small hierarchical system.

And the system does the following.

We have these processes.

P1 up to Pn at the bottom.

They get triggers.

All these triggers are the same.

Whenever they get a trigger, they report that to the layer above.

So P1, after getting a trigger reports to W1 that it got a trigger.

And W1 will then report it to M, and

M does nothing else than simply reporting the trigger upwards.

If we hide all intermediate communication, so

only the triggers at the bottom and the triggers at the tops remain visible,

then the question is what is the size of the whole state space?

That's the first number in the answers.

The second question is what is the size of the system modulo branching bisimulation?

That's the second number in the answers.

And the third question is what is the largest intermediate state

space if we generate the state spaces compositionally and

reduce them modulo branching bisimulation.

And that is the third value in the answers.

So what did we see?

The first observation was that if we have large systems,

then it's a good idea to design them in a hierarchical way, because then you can

generate the whole state space by doing compositional state space generation and

intermediate reductions modulo branching bisimulation.

This works much better than just generating the state space

of the whole thing as a whole in general.

But you can do even better, if you design explicitly

the expected external behavior of all intermediate components,

and you adapt the individual subcomponents such

that they realize exactly this expected behavior.

And if you do so, I think you are among the best if it comes

to design of complex behavior of these kind of systems.

This brings us to the end of this fourth MOOC, and I hope

that you have learned how to specify the requirements for realistic systems.

I hope you have a feeling that you can specify realistic systems and

in particular,

do this in such way that you can avoid the state space explosion problem.

And this means that you are now ready to bring your knowledge into practice.

And that is what we will do in the next MOOC.

There, I will ask you to design a controller for a realistic system.

And what you have to do is first write down the requirements, then make a model

of the system, prove that your model satisfies the requirements.

And this means that you have a design already for

an implementer to build a trustworthy system.

Hope to see you in the next MOOC.

[MUSIC]

Compositional design ; specify external behaviour

System Validation (4): Modelling Software, Protocols, and other behaviour

Meet the Instructors