System Validation is the field that studies the fundamentals of system communication and information processing. It allows automated analysis based on behavioural models of a system to see if a system works correctly. We want to guarantee that the systems does exactly what it is supposed to do. The techniques put forward in system validation allow to prove the absence of errors. It allows to design embedded system behaviour that is structurally sound and as a side effect enforces you to make the behaviour simple and insightful. This means that the systems are not only behaving correctly, but are also much easier to maintain and adapt. ’Requirements by modal formulas' is the third course that shows you how to specify requirements for the automata in order to establish the correct relation between the requirements and the behaviour of the system. Reading material. J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT Press, 2014.
Translation to a Boolean Equation System (BES)
Loading...
來自 EIT Digital 的課程
System Validation (3): Requirements by modal formulas
7 個評分
從本節課中
Advanced modal formulas
This module elaborates on modal formulas. It shows how to use data in the formulas which makes modelling of complex properties much easier. Furthermore, it shows how fairness properties can be modelled in the framework using nested fixed point operators. The last lectures introduce parameterised boolean equation systems and boolean equation systems as important technology to establish that a modal formula is valid for a particular specified behaviour.
與講師見面
Jan Friso GrooteFull professor
Mathematics and Computer Science, Eindhoven University of Technology
Welcome again. In this lecture,
I will introduce Boolean equation systems,
which are the workhorse to determine whether
a modal formula is valid on a labeled transition system.
So, let's look at this labeled transition system
with two states and three transitions, labeled it an a,
a b and a c. And take this as
an example on which we want to verify a particular modal formula.
And for the modal formula,
we take a rather arbitrary one,
but one that you already know, namely,
the formula that says that whenever we can do an a,
then a b will absolutely follow.
And that's this formula.
So this [true* a] and then this typical minimal fixed
point formula that negate B.
If you want to solve this,
then one technique is to translate
the modal formula and labeled transition system to a Boolean equation.
So let's ask ourselves what a Boolean equation is.
So a single Boolean equation is this one,
where we have X as a Boolean variable – that variable can be either true or false.
You have is phi.
Phi is an Boolean expression without negation,
and mu is the minimal fixed point operator.
So we are interested in a minimal Boolean value for X,
such that X is equal to phi.
And we also have a maximal fixed point operator,
so we can also write mu X is equal to phi.
And phi is typically true,
false, X itself, the and or the or.
And we cannot use negation the right-hand side
because then the formulas would not be monotonic anymore.
We are particularly interested in sequences of Boolean equations.
And I'm using the word sequence on purpose and not
set because the order of these Boolean equations is important.
So a typical example is this one,
where we have two equations: mu X is X or Y,
and mu Y is X and Y.
If you look at a Boolean equation,
then we can ask ourselves what the solution is.
So, mu X is X has two solutions,
namely, x is equal to true and x is equal to false.
And what we do is,
due to this minimal fixed point operator,
is that we select the minimal solution.
And if we would write the same with the maximal fixed point operator,
and what we see is a nu X is equal to X.
And we select this solution,
X is equal to true.
If we take more complex sets then we can follow the semantics of the solution.
There's only one single solution for this Boolean equation systems.
And as an illustration,
I will follow the definition of the semantics,
but this is a somewhat cumbersome procedure and,
therefore, it's not really practical to solve these Boolean equation systems.
But let's simply do it.
So, the semantic says that we have two options for X in this Boolean equation system,
namely X is false and X is true, that we can try.
And we will simply try to figure out whether X is false and X is true are solutions.
Now, if you go to left side,
then X is equal to false can be used to simply find equations.
So we replace X by false,
and then we get mu X is equal to false or Y.
And if you even simplify find the second one,
then we get nu Y is equal to false.
And then we can see that there's only one solution for Y.
We can substitute that solution for Y in the first equation,
and we see that X is false is also a solution,
that X becomes false,
and that shows that X is false is a solution.
In the same way we can do this for in the case where X is equal to true.
So, we substitute X is equal to true in the equations and we get
these two new expressions.
And we see in particular that we have nu Y is equal to Y.
And we know there are two solutions for Y.
But due to the maximal fixed point operator,
we have to select the maximal one.
So Y is equal to true is the solution for the second equation.
And then we substitute that back.
In the first equation,
we see that X is equal to true,
and that means that X is equal to true is still a solution of this equation.
So we have X is false being a solution,
X is true being a solution.
And now this minimal fixed point operator kicks in and it
selects the minimal solution of the two.
So what we do is we take X is equal to false,
and as a consequence Y is equal to false,
and that's the solution for this set of two Boolean equation systems.
Typically, we encounter Boolean equation systems of
hundreds of thousands or even many millions of equations.
Now, let's ask ourselves how we can use
these Boolean equation systems to solve this modal formula.
So, what do we do?
Let's copy it to the next slide.
Oh, let's first eliminate the regular formulas.
So the first, true* is being replaced by this maximal fixed point operator.
And let's now take this new modal formula to
next slide and let's try to solve this.
In order to solve this,
I want to give a name to both states.
So here we have state s_1;
here we have state s_two.
And I want to introduce four variables,
Y_1, Y_2, X_1 and X_2.
And Y_1 means that the formulas starting with nu Y is valid in state one,
Y_2 means the formula starting with nu Y is valid in state 2.
And the same holds for X_1 and X_2, namely,
X_1 means the formula starting with mu X is valid in state 1,
and the formula starting with mu – and X_2
means the formula starting with mu X is valid in state two.
So, how does this look like?
Well, we get four equations,
and the fixed point operator for Y carries over to Y_1 and Y_2,
and the fixed point operator for mu carries over to X_1 and X_2.
And if you look at Y_1,
then the question is,
what is the shape of the right-hand side?
And this follows the modal formula.
So let's look at the first part of the modal formula.
And this says that whenever I am in a state,
whenever I can do an action in that state,
Y should hold in the resulting state.
So in state s_1, I can only do an a and end up in state s_2.
So, for this to be valid,
Y should be valid in s_2,
so the right-hand side of the first equation should become Y_2.
And now we can look at the second part of this equation.
So this says whenever we can do an a transition in state s_1,
mu X should become valid in s_1.
So, in s_2, sorry.
So, X_2 should be valid.
So what we see is that in the right-hand side,
we require that X_2 is valid.
And this is the whole equation that results when trying
to verify to see that Y holds in s_1.
Now let's look what happens if Y_2... of what's necessary to make Y_2 valid in state s_2.
So, if you look at the first part of the formula again,
then we have to look at any outgoing transition from s_2.
So, b and c. So,
first let's look at b.
And after doing b,
formula Y should be valid in state s_1.
So this gives rise to the following part of the modal formula
of the Boolean equation system, Y_1.
And if we do that, see,
see that we end up in s_2,
and Y should be valid in s_2.
So, here we get in the right-hand side Y_2.
Then we look at the second part of the formula.
So, whenever we do an a action in state s_2,
but we cannot do an a action,
well, something must hold.
As we cannot do this a action,
the resulting requirement is simply true.
Well, in this way, we can also give the rest.
So for X_2, it's actually that X_2 should be equal to X_1 and true.
And because X_1 does not occur in the right-hand side of any of the other equations,
we can simply ignore it.
Now the question is,
what's now the solution of this Boolean equation system?
I will deal with that in the next lecture.
But, for the moment,
I can say that solution is actually Y_1 is
equal to false and all the others are also equal to false.
So, given that Y_1 is equal to false,
we see that the formula is not valid in initial state,
and that's exactly what we already observed in the beginning,
namely that this formula does not hold for this transition system.
So let's look at an exercise.
We already saw that this particular formula that we were looking at was too
strict to express that b should follow a if c can come in between.
So we had this somewhat weakened formula that says that whenever we can do an a,
we will be able to do a b as long as no b is done.
And if you would apply exactly the same procedure to this formula,
on this transition system, the question is,
what is the boolean equation system that we will obtain?
So what did we show? We introduce the notion of a Boolean equation system as
sequences of simple Boolean equations with maximal and minimal fixed point operations.
And we sketched how a modal formula – together,
with a transition system can be transformed to
a Boolean equation system such that the solution of the Boolean equation system is
exactly an indicator on whether the modal formula is valid for this transition system.
In the next lecture,
I want to explain how you can solve a Boolean equation system.
