Okay.

Well, then hello and welcome everybody to the first tutorial lesson of formal methods

and software engineering.

So let's first start with the, well, no, it already doesn't work anymore.

No, it works.

Let's first start with some organizational stuff.

You already know that the homework in this tutorial, in these tutorials will make up

50% of your grade.

So 50% comes from the homework exercises and 50% from the oral exam at the end of the semester.

Some exercise sheets will appear regularly.

I don't know yet if it's going to be really weekly or if there are going to be larger

exercises which require more than one week to solve.

And these larger exercises would also then probably have to be handed in groups instead

of individually.

And I think I will continue with the practice that I had last year that submission will

be just by email.

My email address will also be on the exercise sheets and you can just send an email before

the next tutorial with your solutions.

There are going to be some theoretical exercises probably even on the first sheet to bridge

the gaps between the lecture and the tutorials.

But most of the exercises will be programming exercises or modeling exercises.

And in class, of course, we will discuss the homework.

We will present solutions that are to some extent special or interesting and we will

compare them and discuss problems that you had in the homework.

So it's not the case that you always have to have everything correct in order to get

full points but it's more that you understand what you're doing because sometimes it's

also difficult to get it right.

And this is an inherent problem of this verification business.

And of course then we will experiment with the tools during class and learn new features,

new commands, new constructs.

But of course it's also important that you actively participate and if you have any interesting

questions then just ask and we can maybe find out something more interesting about what

we're doing.

Okay, no but any questions about the organizational business?

If not then we're going just to start with model checking and temporal logic.

So it should have transpired by now that this is what we are dealing with in the first part

of this lecture.

So we're doing a special kind of model-based verification.

So I subsumed it here under model-based verification techniques which can have different manifestations.

So what they all have in common is that we describe a system and its behavior in some

mathematically precise and unambiguous manner.

And then we use algorithms to explore the states of these models and probably all possible

states of these models.

And there are three different ways to do this.

So the first one is model checking which we are doing here in the course which is an exhaustive

search of these states.

So we build the state graph, we build the complete finite state machine and then we

run a program that exhaustively checks if some property holds in any of these states

or in all of these states.

Then a second method would be simulation, which is what we are not doing and which is