Symbolic Model Checking of Deadlock Free Property of Task Control Architecture(Special Issue on Test and Verification of VLSI)

スポンサーリンク

概要

• 論文の詳細を見る

• This paper describes an efficient symbolic model checking algorithm for verification of deadlock free property of high level robot control program 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 of many concurrent processes such as deadlock free property, 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.

• 社団法人電子情報通信学会の論文
• 2002-10-01

著者

• Hiraishi Hiromi

  Faculty Of Engineering Kyoto Sangyo University

関連論文

• Formal Verification of Totally Self-Checking Properties of Combinational Circuits
• An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System (Special Issue on VLSI Testing and Testable Design)
• Temporal Verification of Real-Time Systems
• Towards Verification of Bit-Slice Circuits : Time-Space Modal Model Checking Approach
• Symbolic Model Checking of Deadlock Free Property of Task Control Architecture(Special Issue on Test and Verification of VLSI)

スポンサーリンク