The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Este artigo descreve um algoritmo eficiente de verificação de modelo simbólico para verificação da propriedade livre de deadlock de um programa de controle de robô de alto nível chamado Task Control Architecture (TCA). TCA é um modelo de processos de controle de robôs simultâneos. A ferramenta de verificação que utilizamos é o Verificador de Modelo Simbólico (SMV). Como o SMV não é tão eficiente para verificação das propriedades de atividade de muitos processos simultâneos, como a propriedade livre de deadlock, primeiro descrevemos a propriedade livre de deadlock usando propriedades de segurança que o SMV pode verificar com eficiência. Além disso, modificamos o algoritmo de verificação do modelo simbólico do SMV para que ele possa lidar com muitos processos simultâneos de forma eficiente. Medições experimentais mostram que podemos obter uma aceleração de mais de 1000 vezes por esses métodos.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -