Symbolic Model Checking of Deadlock Free Property of Task Control Architecture
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E85-D No.10 pp.1579-1586
- Publication Date
- 2002/10/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Test and Verification of VLSI)
- Category
- Verification
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Hiromi HIRAISHI, "Symbolic Model Checking of Deadlock Free Property of Task Control Architecture" in IEICE TRANSACTIONS on Information,
vol. E85-D, no. 10, pp. 1579-1586, October 2002, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e85-d_10_1579/_p
Copy
@ARTICLE{e85-d_10_1579,
author={Hiromi HIRAISHI, },
journal={IEICE TRANSACTIONS on Information},
title={Symbolic Model Checking of Deadlock Free Property of Task Control Architecture},
year={2002},
volume={E85-D},
number={10},
pages={1579-1586},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={October},}
Copy
TY - JOUR
TI - Symbolic Model Checking of Deadlock Free Property of Task Control Architecture
T2 - IEICE TRANSACTIONS on Information
SP - 1579
EP - 1586
AU - Hiromi HIRAISHI
PY - 2002
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E85-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 2002
AB - 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.
ER -
English
