Action Recognition is a fundamental task in computer vision field, with a wide range of applications in autonomous driving, security monitoring, etc. However, previous action recognition approaches usually suffer from the inappropriate spatio-temporal modeling or high computational consumption (e.g., 3D CNN). In this paper, we propose a novel Spatio-Temporal Adaptive Network (STANet) with bidirectional temporal difference, consisting of a Temporal Adaptive module (TA) and a Spatial Adaptive (SA) module, to sufficiently extract the crucial motion information and model the spatial pivotal appearance information from both forward and backward perspectives, respectively. Specifically, the Temporal Adaptive module uses bidirectional temporal differences to learn valuable motion trends and balance the static semantics and dynamic motion for a certain action during information fusion; while the Spatial Adaptive module uses the bidirectional temporal difference to obtain the spatio-channel attention to stress the discriminative position-relevant and semantic-relevant appearance features. Extensive experiments conducted on widely-used action recognition benchmarks UCF-101, HMDB-51, Something-Something V1, and Kinetics-400 prove the effectiveness of the proposed methods compared to other state-of-the-art approaches.

The model-based approach has been widely applied to the design of software. However, most of these approaches depend on simulation and manual code implementation, which reduces the efficiency and quality of software. In this paper, we present a new model-based approach, which automatically generates the executable C++ code running on the popular Robot Operation System (ROS). Our approach consists of three phases: modeling, verification, and automatic code generation. In the modeling phase, the internal interaction behaviors of robot systems are modeled as a network of timed automata. In the verification phase, the safety requirements are formalized and verified. In the code generation phase, a code generation tool can generate executable C++ code from the verified timed automata model. It bridges the gap between the formal model and the error-prone system implementation. Compared with existing method, the code generator provides the abstractions and mapping of ROS instructions, which realize the seamless connection between the generated code and ROS. The tool also supports most of the complex structures and advanced features of timed automata such as timer, committed location, and synchronous action. For evaluation, a real-industrial robot application of grasping a cup is conducted using our model-based design method, and the generated code can be directly deployed and successfully accomplishes the grasping task.

Robot systems have been widely used in industry and also play an important role in human social life. Safety critical applications usually demand rigorously formal verification to ensure correctness. But for the increasing complexity of dynamic environments and applications, it is not easy to build a comprehensive model for the traditional off-line verification. In this paper, we propose $RobotRV$, the first data-centered real-time verification approach for the robot system. Within this approach, a domain-specific language named $RoboticSpec$ is designed to specify the complex application scenario of the robot system, the data packets transmitted in the robot system, and the safety critical temporal properties. Then, we develop an engine to automatically translate the $RoboticSpec$ model into a real-time verifier. The generated verifier serves as an independent plug-in component for the runtime verification of concerned temporal properties. We applied the proposed approach to a real robot system. As presented in experiment results, our method detected potential failures, and improved the safety of robot system.

Obstacle avoidance is a key performance of mobile robots. However, its experimental verification is rather difficult, due to the probabilistic behaviors of both the robots and the obstacles. This paper presents the Markov Decision Process based probabilistic formal models for three obstacle-avoidance strategies of a mobile robot in an uncertain dynamic environment. The models are employed to make analyses in PRISM, and the correctness of the analysis results is verified by MATLAB simulations. Finally, the minimum time and the energy consumption are determined by further analyses in PRISM, which prove to be useful in finding the optimal strategy. The present work provides a foundation for the probabilistic formal verification of more complicated obstacle-avoidance strategies.

Intelligent robots are a current application in Industrial Internet of Things (IIoT), with their trustworthiness being a topic of considerable research interest. Vulnerabilities in robot software may affect the trustworthiness of robotics. To detect these vulnerabilities in robot software, this study proposes a differential fuzz testing method. The main idea is to continuously execute test cases for different versions of software packages to detect inconsistencies among outputs and eventually discover vulnerabilities. First, test cases are generated, combining seed generation and mutation, after which the measured model of the packages in RVIZ is built and the generated seeds are executed. The differences among inconsistent outputs are calculated and the causes of the differences analyzed. Two evaluation metrics for the inconsistencies and seeds are presented. This method is applied to the crucial package in ROS-MoveIt!. The results show that the arm.go() of moveit_commander has joint angle overflow.

Cyber physical system (CPS) is a multi-dimensional complicated system integrating computing, communication and physical environment. CPS is widely used in safety-critical areas such as aerospace, intelligent transportation and medical equipment. So ensuring the security and reliability of CPS is of great significance. Formal verification is one of the useful ways. This paper builds timed automata models for the communication process of CAN bus used in CPS. Our research especially analyses the gateway in the communication process, and simulates the transmission with different rates between the external environment and internal unit. The task also takes into account the packet transmission priority. The model checking tool Uppaal is used to verify the functional and real-time properties. The verification results illustrate that the established model can meet the relevant properties, and the packet can be transmitted in an orderly and efficient manner.