NDLI: Formal verification of a collision-free algorithm of dual-arm robot in HOL4

Content Provider	IEEE Xplore Digital Library
Author	Liming Li Zhiping Shi Yong Guan Chunna Zhao Jie Zhang Hongxing Wei
Copyright Year	2014
Description	Author affiliation: Beijing Key Lab. of Electron. Syst. Reliability Technol., Capital Normal Univ., Beijing, China (Liming Li; Zhiping Shi; Yong Guan; Chunna Zhao) \|\| Sch. of Mech. Eng. & Autom., Beihang Univ., Beijing, China (Hongxing Wei) \|\| Coll. of Inf. Sci. & Technol., Beijing Univ. of Chem. Technol., Beijing, China (Jie Zhang)
Abstract	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.
Starting Page	1380
Ending Page	1385
File Size	243402
Page Count	6
File Format	PDF
ISBN	9781479936854
DOI	10.1109/ICRA.2014.6907032
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2014-05-31
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Manipulators Collision avoidance Joints Safety Planning Educational institutions
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A safety arc based collision avoidance algorithm of a two-arm robot manipulator

Development of manipulation planning algorithm for a dual-arm robot assembly task

Sampling-based safe path planning for robotic manipulators

Dynamic efficient collision checking method of robot arm paths in configuration space

Real-time collision avoidance in human-robot interaction based on kinetostatic safety field

An Alternate Priority Planning Algorithm for Dual-Arm Systems

Walking assist design of a dual-arm robot

System for automatic collisions prevention for a manipulator arm of a mobile robot

Collision-avoidance planning of soccer robot in RoboCup3D simulation environment

Formal verification of a collision-free algorithm of dual-arm robot in HOL4

Similar Documents

A safety arc based collision avoidance algorithm of a two-arm robot manipulator

Development of manipulation planning algorithm for a dual-arm robot assembly task

Sampling-based safe path planning for robotic manipulators

Dynamic efficient collision checking method of robot arm paths in configuration space

Real-time collision avoidance in human-robot interaction based on kinetostatic safety field

An Alternate Priority Planning Algorithm for Dual-Arm Systems

Walking assist design of a dual-arm robot

System for automatic collisions prevention for a manipulator arm of a mobile robot

Collision-avoidance planning of soccer robot in RoboCup3D simulation environment

Formal verification of a collision-free algorithm of dual-arm robot in HOL4