Robot Operating System(ROS) is widely used in the development of various service robots, which have high requirements in safety and reliability. Data distribution service(DDS) is deployed in ROS2 to implement the control of nodes and data distribution, which is very important for the operation of application on ROS2. In this paper, we focus on model abstraction, formal modeling and automatic verification for DDS in ROS2. A distributed model with interface parameters was established in PRISM. Properties such as security, liveness and priority of DDS in ROS2 were verified. The results show that the design satisfies these properties and high-priority messages can be sent and transmitted preferentially by the system. Due to the experiment result, we come up with a suggestion that the system will be better if its buffer can store six messages or more.

Embedded systems are becoming increasingly popular due to their widespread applications. Hardware/software partitioning with reliability in consideration is becoming one of the most crucial steps in the design of complex embedded systems, especially for safety critical applications. In this paper, a reliability-centric approach is proposed to increase the reliability and decrease the potential errors of the embedded system during the partition stage. We use task graph to model the system function blocks, and treat reliability as the first-class metric during the mathematical formalization and optimization procedure. Experimental evaluations demonstrate that the proposed approach obtains a better solution with the trade off of time, cost and reliability compared to existing partitioning methods, with higher and more accurate reliability characterization for safety-critical systems.

Wearable inertial tracking is well accepted due to its convenience for free-style motion tracking with high accuracy. Traditionally, complicated high-order calculations for human kinematic modeling and inaccurate estimation of sensor placement are interfering the efficiency of real-time tracking. In order to tackle the challenges, a wearable human motion tracking system is developed by applying twists and exponential maps techniques. When the body segments are articulated by product of exponential maps, joint positions are continuously updated based on these techniques and their rotational angles are represented individually within the global frame. It is more efficient to achieve real-time motion tracking with low-order calculations. Meanwhile by applying the well-designed calibration procedure, it is more convenient to estimate a sensor's position and orientation regardless of knowing its placement. This paper presents our approach and exemplifies the assessment of proposed motion tracking system by several tests of limb and full body motion tracking. The comparisons with Vicon and OptiTrack motion capture systems verify satisfactorily high accuracy.

Motion planning is an important problem with many applications in robotics. In this paper, we focus on motion planning with rectangular obstacles parallel to the X, Y or Z axis. We formulate motion planning using Satisfiability Modulo Theories (SMT) and use SMT solvers to find a feasible path from the source to the goal. Our formulation decompose the robotic path into N path segments where the two ends of each path segment can be constrained using difference logic. Our SMT approach will find a solution if and only if a feasible path exists for the given constraints. We present extensive experimental results to demonstrate the scalability of our approach.

Possessing two manipulators heightens the ability of dual-arm robots (DAR) to conduct complex tasks, while raising hazard that the two manipulators might collide with each other or with other objects. DARs are usually equipped with a collision-free motion planning algorithms (CFMPA) to prevent the two manipulators from colliding. The CFMPA searches the motion paths of robot manipulators, which are expected to be as short and smooth as possible under the premise of ensuring safety. It is important to ensure that the algorithm is correct and efficient. It is not enough to apply traditional test methods to determine whether DARs can work in safety-critical applications. In this paper, theorem proving technology is employed to analyze the correctness and efficiency of a classical CFMPA. The CFMPA is outlined, and then formalized in high order logic with the theorem prover HOL4. An inconsistency in the range of motions of the robot manipulators in the algorithm is discovered. An improved algorithm is therefore proposed. Formal verification with HOL4 proves the correctness and efficiency of the proposed algorithm that has already run on a real DAR as well, in conformity with our expectation.

In designing robot control systems, simulation is still the primary approach to verifying the functions of circuit descriptions written in hardware design language. The validity of the verification depends on the coverage metric. But not all state spaces can be specified in a simulation. Model checking can overcome the shortcomings of simulation, because all of the state spaces can be traversed. Robot control system is an important part of the robot, used in the control of the manipulator to perform specific tasks. Therefore, in this paper a verification framework is presented for design correctness of robotic manipulator, which combines simulation and model checking. The framework is also applied to other control system or control hardware. Model checking guides the generating of test vectors, and makes the functional coverage reach 100% quickly. In this paper, a manipulator designed with six degrees of freedom is verified. The results of the verification of the manipulator show that the verification framework is effective for checking the design correctness of robotic manipulator.

Sambot is a module robot system, with the advantages of self-assembly. A target robotic configuration can be organized by a group of Sambots. A novel motion planning method for Sambot configuration using model checking is presented in this paper. This hierarchical method contains two layers. The abstract logic layer is responsible for the discrete planning of Sambots configuration. The robot and the environment are all modeled as timed automata. System requirements are formalized as Computational Tree Logic (CTL) formulas. Model checking is applied on the system model. The verification result gives the optimal discrete plans for the configuration of Sambot. In physical layer, a sample-based planner generates the trajectory trace considering the dynamics of Sambot and the suggested high level plans. The experiment results illustrate the effectiveness of our approach.

Programable logic controllers (PLCs) are complex embedded systems which are widely used in industry. The formal modeling of PLC system for verification is a rough task. Good verification model should be faithful with the system, and also should have suitable scale because of the state explosion problem of verification. This paper proposes an automatic framework for the construction of verification model of PLC systems. BIP (Behavior, Interaction, Priority) separates behavioral and architectural aspects in modelling. Specifical PLC features and system architecture are modelled by BIP framework. They are universal for all PLC applications. We define the operational semantics of PLC instruction and present an automatic translation based modeling method for PLC software. A small example is demonstrated for our approach.

Robust navigation for mobile robots requires an accurate method for tracking the robot position in the environment. This paper presents a simple and novel visual-inertial integration system suitable for unstructured and unprepared indoor environments, where MARG (Magnet, Angular Rate and Gravity) sensors and a monocular camera are used. The pre-estimated orientation from MARG sensors, is used to estimate the translation based on the data from the visual and inertial sensors. This has a significant effect on the performance of the fusion sensing strategy and makes the fusion procedure much easier, because the gravitational acceleration can be correctly removed from the accelerometer measurements before the fusion procedure, where a linear Kalman Filter is selected as the fusion estimator. the use of pre-estimated orientation can help to eliminate erroneous point matches based on the properties of the pure camera translation and thus the computational requirements can be significantly reduced compared to the RANSAC (RANdom SAmple Consensus) algorithm. In addition, an adaptive-frame-rate single camera is selected to not only avoid motion blur based on the angular velocity and acceleration after compensation but also to make an effect called visual zero-velocity update for the static motion. Thus, it can recover a more accurate baseline and meanwhile reduce the computational requirements. In particular, an absolute scale factor, which is usually lost in monocular camera tracking, can be obtained by introducing it into the estimator. Simulation and experimental results are presented for different environments with different types of movement and the results from a Pioneer robot are used to demonstrate the accuracy of the proposed method.