DocumentCode :
2752584
Title :
Verification of deadlock free property of high level robot control
Author :
Hiraishi, Hiromi
Author_Institution :
Kyoto Sangyo Univ., Japan
fYear :
2000
fDate :
2000
Firstpage :
198
Lastpage :
203
Abstract :
This paper describes an efficient verification algorithm for deadlock free property of high level robot control called Task Control Architecture (TCA). TCA is a model of concurrent robot control processes. The verification tool we used is the Symbolic Model Verifier (SMV). Since the SMV is not so efficient for verification of liveness properties such as deadlock free property of many concurrent processes, we first described the deadlock free property by using safety properties that SMV can verify efficiently. In addition, we modify the symbolic model checking algorithm of the SMV so that it can handle many concurrent processes efficiently. Experimental measurements show that we can obtain more than 1000 times speed-up by these methods
Keywords :
concurrency control; formal verification; logic testing; message passing; robots; symbol manipulation; concurrent robot control processes; deadlock free property; high level robot control; liveness properties; safety properties; symbolic model checking algorithm; symbolic model verifier; task control architecture; verification algorithm; Boolean functions; Data structures; Logic; Message passing; Process design; Robot control; Robot kinematics; Safety; System recovery;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Test Symposium, 2000. (ATS 2000). Proceedings of the Ninth Asian
Conference_Location :
Taipei
ISSN :
1081-7735
Print_ISBN :
0-7695-0887-1
Type :
conf
DOI :
10.1109/ATS.2000.893625
Filename :
893625
Link To Document :
بازگشت