0:25

So one way of doing that is that you can limit the number of values in your model.

So instead of using a distance,

you could probably replace such a whole domain by a few values, for

instance, near, far, or very far, or something like that, or,

even, just one single distance used, a constant distance.

0:51

You could also consider reducing the input to only a very small number of cases.

You may find that that's not really desired because you would like to know

that your system works well under all circumstances.

But, what one then sees,

is that one cannot prove the correctness of the system anymore and

one has to establish the correctness by, for instance, testing and

by just verifying the equipment for a few input values.

You find many more problems and uncover far more books then by just testing.

So, it's far more effective to check the system for

just a restricted number of input values, if you can not check them for all.

Actually, it is the case that if you have a realistic system,

then the number of dates are often so

big that it is extremely time consuming to do a verification.

And a very good strategy is to actually restrict all

your data domains to trivial data domains, then do a first round of verification,

if that succeeds, slowly increase the size of your data domains.

If you have to wait for verification for more than a few minutes,

then your data domains are generally too big.

So let's look at a concrete example.

Here we have a car that approaches a movable barrier, and

there is a distance detector with an associated controller, and

the distance detector measures the distance to the car,

and if the car will pass the movable barrier

during the next measurement, then it will quickly open the barrier, and

we assume that opening the barrier does not really take time.

2:51

This is the controller, it has two actions.

It measures the distance with an action distance, d, and

it triggers the barrier to open with the action trick.

The maximal distance, that can be measured as m, m as in it's file number,

and we take m to be 100, in this particular case.

And behavior of the whole system is described by this line,

where you can see this process distance controller.

And it recalls the previous distance that was measured.

Initially, this previous distance is set to the value, m,

that's the maximal measurable distance.

3:39

And if the distance is smaller, of if two times the distance is smaller

than the previous measured distance, then the car will pass the barrier before

the next measurement, so the trigger action should be sent.

3:57

And if the distance, two times the distance is larger or

equal than the previous distance, the car will not pass the barrier and

the just measured distance will actually store it into the previous distance and

the process will repeat itself again.

4:18

What we see is that the state space is actually 10,000 states big,

and this is quite amazing for such a simple system.

And the reason for that is, that at this particular spot,

4:40

And what we also see is that the only information from the distance and

the previous distance that is actually being used is this condition.

So its only a Boolean information,

namely that 2d is smaller than the previous d or not.

5:28

The second action dist means that we measure the distance,

while the car will not pass the barriers during the next measurement.

And then, we just give this just measured distance,

d, as an argument to the distance control to be recalled for the next round.

What we see is that we only need to record the value d here.

And that has an effect that the state space of this whole system is only handled

in one states big, and that is substantially smaller

than the 10,000 of the previous state space by just moving a condition.

6:32

So we have now the abstract distance controller and

it reads the distance, if the distance is near,

it sends the trigger, otherwise it simply repeats itself and the initial

state is just ADC without a parameter, because that is not needed anymore and

what we see is that the whole state space is only two states big.

So here, we have an exercise and

what's very useful is that one can measure upper bounds

on the states space by looking at the size of the data domains in the linear process.

So, the question here is, if this is our linear process with four parameters and

that domain, D1, has 7 elements, D2 and D3 have both 10 elements,

7:35

We looked at data and we should be very careful with data as otherwise,

we'll get a state space explosion.

So, if possible, our data domains should be made as small as possible,

or even better, one should replace the data domains by abstract

data domains with abstract values, if that leads to smaller domains.

8:01

One can increase the size of the model by storing

data at places where one may not be aware of that.

So sometimes it may help to investigate the model for these stored places of

data and reduce the size by, for instance, moving conditions to another place.

If the state space is still too big,

once you've seriously considered to verify the system under very strict

scenarios where the environment can only offer a limited amount of values, and

the reason for this is that it is far more effective

to analyze a system using model checking under all kinds of scenarios,

9:03

And the last thing is that once you start by extremely

reducing the data in the model, when one starts verifying the reason for

this is that if you can't verify your system under usual circumstances,

you'll certainly not be able to do it, then the data domains become larger.

And if you find yourself waiting for

the response of the tools to do a verification for

more than a few minutes, and you have no idea how long it will take, then probably,

you should first consider reducing your data domain.

In the next lecture, I will address sequentializing

the behavior of parallel components, to reduce the size for the state space.

Thank you for watching.

[MUSIC]