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]

Â