Skillset Verification
The main objective of this verification is to independently check the different elements of the skillset. We seek to show by this verification that the different elements of the model are correctly defined. The notion of resource is a cornerstone of the semantics of skills. Indeed, it constrains the guards, the effects present in the events, and the skills and consequently impacts the whole behavior of the skillset. Thus, the skillset model verification consists in checking that the guards make sense, and checking that the effects are possible. It is important to note that, even if these checks fail, the system will run without crashing and the execution has a predictable and correctly defined behavior. But it is likely that this behavior is not the desired one and can be associated with an ‘erroneous’ specification.
Guard Verification
The first check is on the guards. We formally check that the guards make sense. That is, they can be true or false. More precisely, since the guards relate to the state of the resources, we seek to verify that there is at least one configuration of the resources in which the logical formula of the guard is evaluated as true and at least one configuration in which it is evaluated as false. The guards are present in the events, preconditions and invariants of the skills.
To solve this problem, we use the Sat Modulo Theory formalism, as it allows us to represent problems involving logical formulas and some structured data useful for our modeling. Each resource is represented with a Sort DataType (Enum) which contains all the states of the resource. The transitions of the state machine are represented by a function that indicates whether there is a transition between two states. The current state of each resource is translated by a corresponding spell constant. The guard formulas are simply translated following their semantics. To check if the guard holds, its corresponding constraint is added to the solver. Then we can ask the solver if the system has a solution. If a solution exists, we can ask for the state of the variables and thus find the state of the resources that lead to the satisfaction of the model.
Event Verification
The method presented above is applied to the guard of each event, in order to determine whether it can be evaluated as true. In the following example, the verification indicates that the guard of the event E cannot fail.
1 skillset S {
2 resource R {
3 state {A B}
4 initial A
5 transition all
6 }
7
8 event E {
9 guard R == A or R == B
10 effect R -> B
11 }
12 }
Skill precondition and invariant
In the skills, the guards are present in the preconditions and invariants. However, unlike those present in events, they are linked together. Indeed, the preconditions (resp. invariants) are evaluated in the order of their declaration in the model. Consequently, to test the usefulness of a precondition (resp. invariant), all the previous preconditions (resp. invariant) must be satisfied.
In the following example, the verification indicates that both preconditions cannot be true at the same time.
1 skillset S {
2 resource R {
3 state {A B}
4 initial A
5 transition {
6 A -> B
7 }
8 }
9
10 skill S {
11 precondition p1: R == B
12 precondition p2: R == A
13 }
14 }
In the following example, the verification indicates that second invariant cannot fail.
1 skillset S {
2 resource R {
3 state {A B C}
4 initial A
5 transition {
6 A -> B
7 A -> C
8 }
9 }
10
11 skill S {
12 precondition p: R == A
13 start R -> B
14 invariant p1 {
15 guard R == B
16 }
17 invariant p2 {
18 guard R != A and R != C
19 }
20 }
21 }
Effects Verification
The second check is on the effects. We have shown in the previous section that the execution semantics of the specification language is well-defined, whether the effects can be realized or not. However, in the general case, when effects are specified, it is important that they are realized. Therefore, it is essential to determine whether effects will always be realized or whether there are configurations in which they may fail.
To analyze the effects, we use the same method as for the guard study. We create an SMT model of the resources, the guards, the effects, and using the solver, we look for a counter-example that shows a configuration in which the analyzed effect can fail.
Event Verification
The effect of an event can fail if there is a solution to the SMT problem in which the guard is satisfied, and there is at least one arc of an effect that is not feasible.
To illustrate effect failure detection, let’s consider the take_authority event we defined earlier. We will voluntarily introduce an error in the effects by slightly modifying the state machine of the ‘authority’ resource by no longer allowing the pilot to take control when the drone has the commands. The following listing shows the new state machine of the resource.
1 resource {
2 authority {
3 state { Pilot Free Software }
4 initial Pilot
5 transition {
6 Free -> Software
7 Free -> Pilot
8 Software -> Free
9 Pilot -> Free
10 }
11 }
In this example, the verification highlights an effect error. Indeed, if the resource authority is Software, the effect cannot be applied because there is no transition from the state Software to the state Pilot.
Skill Verification
The same analysis is applied on the different elements of the skills to check their effects: start, invariants; terminates. Moreover, verify if a skill can start and terminates with an invariant failure instantaneously. This verification is shown by the following example.
1 skillset S {
2 resource R {
3 state {A B C}
4 initial A
5 transition {
6 A -> B
7 A -> C
8 }
9 }
10
11 skill S {
12 precondition p: R == A
13 start R -> B
14 invariant p1 {
15 guard R == A
16 }
17 }
18 }