Chapter 2 AFSM-based Reactive Robot Control Systems and Roving Robot Collision
2.2 Roving Robot Collision Avoidance Experiment
2.2.5 Properties To Be Verified
The property we want to check by OMocha is：
Whether the robot will collide with obstacles or walls?
The robot has the two above-mentioned behaviors can wander aimlessly around the environment and try to avoid collision with obstacles. However, the strategy determined by the RRCS for avoiding collision doesn’t guarantee the robot doesn’t collide with obstacles. In the strategy for avoiding collision, the relationship between “Distance away from the obstacles” and “Reverse acceleration” is the most important part.
In order to make sure the behavior of the strategy is the same as our expected behavior, we must describe the property with Temporal Logic and check whether the strategy really makes the robot not to collide with obstacles. The checking procedure is completed by OMocha.
1 “M” is the mass of the robot. “F” is the force generated by motor, “A” is the acceleration
Chapter 3
Model Checking for AFSM-based RRCS, Concepts
After introducing AFSM and roving robot collision avoidance experiment, we’ll explain how to verify an AFSM-based RRCS by model checker. In this section, we will explain the principle of model checking by the verification procedure of model checker, OMocha [4]. The introduction for OMocha is in Section 3.2.
In Section 3.1.1, we will give two examples for explaining the verification procedure. In the two examples, we will use the formal input language for OMocha. The formal input language for OMocha is explained in detail in Section 3.3.
3.1 Verification Procedure
The concept of verification procedure is step by step to explore all reachable states from initial state, and then check whether all explored reachable states which represent the behaviors of programs satisfy the properties.
3.1.1 Two Examples of Verification Procedure
3.1.1.1 Simple ExampleTake a simple AFSM-based system shown in Fig. 3-1 as an example. The AFSM-based system is composed of two AFSM modules. The property we want to check is “AG ((STATE_A=A2 && A_B=false)||(STATE_A=A1 && A_B=true))”. It means whether “((STATE_A=A2 && A_B=false)||(STATE_A=A1 && A_B=true))” is always true from initial state to all reachable states.
The definition of initial state is the combination of all variables’ initial values of a system.
The initial state of the AFSM-based system is { STATE_A=A1 , A_B=false , STATE_B=B1 }.
According to the transition functions(update commands) of the AFSM-based system
described in programs, the sequential state transition of the AFSM-based system is listed as Table 3-1. The next state of the initial state, which is also the 2nd state of the AFSM system is {STATE_A=A2 , A_B=false , STATE_B=B1 }. Then the next state of the 2nd state, which is also the 3rd state of the AFSM system is { STATE_A=A1 , A_B=true , STATE_B=B1 }.
OMocha will keep on exploring the next state of every state. Finally, OMocha will find out that the 2nd to the 5th states are all possible reachable states from the initial state. Then the 6th to the 9th states repeat the value of the 2th to the 5th state, and so on. The all possible states of the system include the initial state and all possible reachable states from the initial state.
During the procedure of exploring all possible states of the system, OMocha detects the behaviors of the programs violate the properties at initial state. Therefore, the behaviors of the programs don’t satisfy the properties.
3.1.1.2 Advanced Example
After understanding the simple example of AFSM-based system, let us consider another advanced example. In the advanced example, transition functions (update commands) are allowed to include non-deterministic choices. As shown in Fig. 3-2, module A has a non-deterministic choice as follow:
[]STATE_A = A2 -> STATE_A’:=A1; A_B’:= true []STATE_A = A2 -> STATE_A’:=A2; A_B’:= true
If the variables’ values of module A are { STATE_A=A2 , A_B=Don’t Care } in current state, the variables’ values of module A may be { STATE_A=A1,A_B=true } or { STATE_A=A2,A_B=true } in next state. The sequential state transition of the advanced AFSM example is listed as Table 3-2. The non-deterministic choices are provided to system designer for simulating the random situation. In order to make the concept more clearly, we illustrate the trace-tree of verification procedure for the advanced example with Fig. 3-3.
In Fig. 2-8, the node which has dotted circle is the state which will determine its next states
according to the non-deterministic choices. Therefore, the trace-tree of verification procedure for the advanced example is a multi-branch tree. However, the trace-tree of verification procedure for the simple AFSM example is a single-branch tree as shown in Fig. 3-4.
Fig. 3-1. Simple example of AFSM-based system variable
state
STATE_A A_B STATE_B
1 A1 False B1
2 A2 False B1
3 A1 True B1
4 A2 False B2
5 A1 True B2
6 A2 False B1
... ... ... ...
Table. 3-1. Sequential state transition of simple AFSM-based system
initial state
all reachable states
Fig. 3-2. Advanced example of AFSM-based system variable
state
STATE_A A_B STATE_B
1 A1 False B1
2 A2 False B1
3 A1 True B1
4 A2 False B2
5 A1 True B2
6 A2 False B1
7 A2 True B1
8 A1 True B2
9 A2 False B1
… … … …
Table. 3-2. Sequential state transitions of advanced AFSM-based system
initial state
all reachable states
Fig. 3-3 Fig. 3-4
Fig. 3-3. The trace-tree of verification procedure of advanced example. The node which has dotted circle is the state which will determine its next state according to non-deterministic choices.
Fig. 3-4. The trace-tree of verification procedure of simple example
3.2 Model Checker：OMocha
The model checker chosen for our research is OMocha [4]. The formal input language for OMocha includes two parts: The first part is programs described by UNITY-based specification language [2], and the second part is properties described by Temporal Logic [5].
After the formal input language is fed into OMocha, OMocha will check whether the behaviors of the programs satisfy the properties. If the behaviors of the programs violate the properties, OMocha will show one counterexample. Otherwise, it’ll show the behaviors of the programs satisfy the properties.
. In Section 3.3, we’ll introduce the formal input language for OMocha.
3.3 Formal Input Language for OMocha
3.3.1 Programs Described by UNITY-based Specification Language
(A) IntroductionIn OMocha, the programs are described by UNITY-based specification language. There are two main reasons about why it uses UNITY to describe the programs as follows：
(1) UNITY could represent the relationship between current state and next state, what is called transition function. Therefore, we could describe an AFSM-based RRCS by UNITY.
(2) In order to operation in coordination with OMocha. In OMocha, the only data types can be defined are cyclic integer and boolean, and the syntax and semantics of UNITY can provide cyclic integer ( e.g., “A: bit[5]”, the range of cyclic integer A is from 0 to 31).
(B) Syntax and Semantics
There are two parts in programs:
(1)Module Description
In the first part of programs, we describe all AFSM modules in module description. For describing a module, it includes two necessary parts: variables definition and atoms definition.
Fig. 3-5. Module description
Variables Definition
In variables definition, there are three kinds of variables can be defined: external, interface, and private.
External variables---The input ports of AFSM module, they receive data from other AFSM modules’ interface variables.
Interface variables---The output ports of AFSM module, they send data to other AFSM modules’ external variables.
Private variables---The local variables of AFSM module, they don’t connect with other AFSM modules.
Three kinds of data types which can be defined for above three kinds of variables are
“cyclic integer”, “boolean” and “enum”.
Atoms Definition
In atoms definition, we describe the init action executed during initial round, and the update action executed during each update round. The initial and update action are specified by the keywords init and update. There are some init commands in initial action, and there are some update commands in update action. An example for atoms definition is shown as Fig. 3-6.
Fig. 3-6. Example for atoms definition
In each update round, every variable x has two values. The value of x at the beginning of the round is called the latched value, and the value of x at the end of the round is called the
updated value. We use unprimed symbols, such as x, to refer to latched values, and primed symbols, such as x’, to refer to the corresponding updated values.
The updated value of (N-1)th round is equal to the latched value of Nth round. The latched value of x is also the current state of x, and the updated value of x is also the next state of x.
The relationship between latched value (current state) and updated value (next state) during neighbor update rounds is shown as Fig. 3-7.
Fig. 3-7. The relationship between latched value and updated value during neighbor
update rounds.
Let us look the example shown in Fig. 3-6, the updated value of STATE and A are init and 1 at initial round. According to the update command in update action, if the latched value of STATE and A are init and 1, the updated value of them will be set to start and 2. Therefore, the updated values of STATE and A are start and 2 at 1st update round. Update commands which determine the relationship between latched values and updated values, can regard as transition functions which determine relationship between current state and next state.
(2) Module Connection
After all AFSM modules are described in module description, we need to describe the connection relationship between these AFSM modules. An interface variable can connect with some external variables of other AFSM modules which have the same name as the interface variable. An external variable can only connect with an interface variable of another AFSM module which has the same name as the external variable.
3.3.2 Properties Described by Temporal Logic
(A) IntroductionIn OMocha, the method chosen to describe the properties of an AFSM-based RRCS is Temporal Logic.
Temporal Logic is used to represent the properties of state transitions of a system over time domain. For instance, we want to check whether variable A is always less than 10 during all possible states. In this case, the representation of Temporal Logic is “AG A<10”, the meaning of ”AG” is “always true” during all possible states from initial state. After describing the programs of an AFSM-based RRCS by UNITY, we can describe the properties of the AFSM-based RRCS by Temporal Logic, and the properties are what we want to check by OMocha. When OMocha receives the formal input language including programs and properties, it can check whether the behaviors of the programs satisfy the properties.
(B) Syntax and Semantics
Every property of a system is described by Temporal Logic. A Temporal Logic formula consists of the propositional logic formula and temporal connectives： The propositional logic formulas are expressions which consist of logical operators and the variables of the system. The temporal connectives are expressions to indicate the subset of future states of the system.
The temporal connectives are pairs of symbols：
The first member of the pair is one of
A - meaning on all paths from the “current” state, read as “inevitably”
E - meaning on at least one path from the ”current” state, read as “possibly”
The second member of the pair is one of X - meaning the next state
G - meaning all future states, read as “globally”
F - meaning some future state U - meaning until
Take “mutual exclusion” as example. Suppose we are talking about two processes P1, P2 that share data. The protocol allows only one process to be in its critical section at any time.
If we want to describe the “mutual exclusion” property by Temporal Logic, the Temporal Logic formula will be described as follow：
AG !( Critical[P1] & Critical[P2] )
The propositional logic formula !( Critical[P1] & Critical[P2]) The temporal connectives AG
This Temporal Logic formula is true iff Critical[P1] and Critical[P2] won’t be true in the meantime for all states on all paths into the future from current state.
Chapter 4
Model Checking for AFSM-based RRCS, Approaches
In this Chapter, we present three approaches to lower the difficulty of formal verification for the experiment. After using the three approaches to reduce the number of states of the RRCS and environment, formal verification can become applicable for the experiment.
4.1 State Space Discretization
A system described on the continuous domain can’t be verified by OMocha, because the number of all possible states is infinite. Before constructing an AFSM-based RRCS we must transform the system and environment from continuous domain to discrete domain. Otherwise, OMocha can’t handle it.
In discretization procedure, there are two parts. (1) Time Discretization, and (2) Space Discretization. Time Discretization has been explained in Section 2.1.1.2, therefore we will only explain Space Discretization in this section. We will give two examples to illustrate the relationship between continuous space and discrete space below.
Take a simple MAP as first example, the continuous MAP whose size is 2*2 m2 is transformed into a discrete MAP. In x-axis and y-axis, the continuous domain is partitioned into 21 points separately (x-axis:0.1.2….20, y-axis:0.1.2….20). Therefore, the distance between two neighbor points is 0.1m, and the size of the discrete MAP is 21*21. The relationship between continuous and discrete MAP is shown as Fig. 4-1.
Fig. 4-1. (a) continuous MAP (b) discrete MAP
Then, we give another example. In Section 2.2.5, we have mentioned that in the strategy for avoiding collision, the relationship between “Distance away from the obstacles” and “Reverse acceleration” is the most important part. In Fig. 4-2, we illustrate the relationship between continuous domain and discrete domain in this example.
Fig. 4-2 (a) continuous domain (b) discrete domain
In Fig. 4-2, “Reverse acceleration” is approximately linear inverse proportion to “Distance away from the obstacles” on continuous domain, the curve presents the relationship between the two parameters. The number of all possible mapping relations of them is infinite, the mapping set includes { (0, 5)..(0.5,4.5)..(3.5,1.5)..(5,0) }. After transformation, the mapping set has only fix points on discrete domain, they are { (0,5) . (1,4) . (2,3) . (3,2) . (4,1) . (5,0) }.
After discretization procedure, the complexity of a system will be simplified to the degree can be handled by OMocha.
4.2 External Function for Computation/State Hiding
In order to improve the capabilities which the UNITY-based programs can support, and reduce the number of states of a system. OMocha provides the external function for system designer. The two main advantages are listed below：
4.2.1 Computation Hiding
The semantics and syntax of UNITY are very basic and aren’t as powerful as high-level language. For this reason, it’ll be very hard to build complicated programs of a system by UNITY.
In order to improve the capabilities which the UNITY-based programs can support, OMocha provides the external function for system designer. The external function is described by C language. The UNITY which includes external function is called advanced UNITY.
In original UNITY, the semantics and syntax can only provide basic capabilities, these basic capabilities include：
Value assignment return value of external function by variables which defined in UNITY.
There are two examples for explaining computation hiding through external function. The two example are listed below：
Example 1
A part of programs described with original UNITY
The same part described with advanced UNITY Example 2
A part of programs described with original UNITY
The same part described with advanced UNITY
4.2.2 State Hiding：Reducing the Number of All Reachable States of a System
How complicated a system can be verified by OMocha depends on the number of all reachable states. Once the number of all reachable states of a system is greater than the limitation of OMocha’s capability, the “out of memory” problem will occur during checking procedure. Therefore, we have to carefully control the complexity of a system so that the resource (memory, CPU speed...etc) of OMocha can handle the checking procedure.
The number of all reachable states of a system depends on the all possible combination of all variables which are defined in UNITY-based programs. If we can move out some variables which are defined in UNITY-based programs, and encapsulate them into external function, the number of all reachable states will reduce.
But, what kinds of variables can be encapsulated into external function ？ During verification procedure, there are some system variables which are irrelevant to behavior verification. For example, in the experiment explained in Chapter 2, OMocha only needs to know the velocity and location of the robot whereas it doesn’t need to know the computation of detecting environment, and determining the degree of acceleration. The variables for detecting environment and determining the degree of acceleration can be exported to external function.
An example of the encapsulation procedure of external function is shown as Fig. 4-3. In Fig.
4-3, the system is composed of four AFSM modules. There is one interface variable in each module, so the total number of the variables in the system is four. According to encapsulation principle, if a module doesn’t include some nondeterministic update commands, it can be encapsulated into a external module. Take the system as a example, the module B, module C and module D can be encapsulated into a external module which invokes a external function to handle all update commands of them, the encapsulation procedure shown as Fig 4-3(c). The module A can not be encapsulated into the same external module, because it includes one
nondeterministic update command. After encapsulation procedure, the system reduces the number of modules from 4 to 2, and reduces the number of variables from 4 to 2. The two interface variables Bout,Cout are encapsulated into the external function “Ext_fun”, so model checker doesn’t need to consider them. In some cases, reducing the number of variables by encapsulation procedure can obviously lower the number of all reachable states of the system and lower the running time of checking procedure, especially in a complicated system.
Fig. 4-3. Encapsulation procedure
(a) A system is composed of four AFSM modules
(b) The module B, module C and module D can be encapsulated into a external module
(c) The three modules will be integrated into one external module, the UNITY-based programs of the external module and C code of external function Ext_fun() are shown in the figure.
4.3 Elimination of Unnecessary Checking Cases
The concept of verification procedure is step by step to explore all reachable states from initial state. Therefore this is a kind of method of exhaustion. However, according to the properties we want to check by OMocha, we can eliminate some unnecessary checking cases, because this part of checking cases will never violate the properties. Take the experiment explained in Chapter 2 as example. The robot will never collide with obstacles while it wanders aimlessly in the range which has no obstacles. Therefore, OMocha can eliminate the part of checking cases.
Chapter 5
Implementation of Roving Robot Collision Avoidance Experiment
In this Chapter, we will present how to construct the AFSM-based RRCS and environment in the experiment with UNITY, and explain the AFSM-based RRCS in detail.
We have explained the chart of an AFSM module in Section 2.1, and explained how to describe the programs of an AFSM module has explained in Section 3.3.1. These two sections are the most important foundations for this section.
In Section 5.1, we will show the full structure of the experiment, and then briefly introduce these AFSM modules in the experiment. In Section 5.2, we introduce every AFSM module in detail, and how these AFMS modules connect with other modules and work in coordination.
In Section 5.3, we explain the “No_Collision” property described by Temporal Logic. The checking results of the experiment are explained in Chapter 6.
5.1 Full Structure of the Experiment
Fig. 5-1 Full structure of the experiment
The full structure of the experiment is shown as Fig. 5-1, the AFSM-based RRCS is
composed of 6 AFSM modules, and environment is composed of 1 AFSM module. These modules are listed in Table 5-1：
Module name Module figure Functionality
MAP
z Set the position of obstacles and walls into
MAP_walls and MAP_obstacles at initial round.
z Provide the map of environment to other modules
z Provide the map of environment to other modules