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
A álgebra de comunicação de recursos compartilhados (ACSR) é uma álgebra de processo temporizado que estende as álgebras de processo clássicas com a noção de recurso. Ao analisar modelos ACSR, as técnicas existentes, como verificação de bisimulação e verificação de modelo Hennessy-Milner Logic (HML), são muito importantes na teoria do ACSR, mas são difíceis de usar na prática para modelos de sistemas grandes e complexos. Neste artigo, sugerimos uma estrutura para verificar modelos ACSR em relação aos seus requisitos descritos em uma lógica temporal temporizada expressiva. Demonstramos a utilidade da nossa abordagem com um estudo de caso do mundo real.
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
Junkil PARK, Jungjae LEE, Jin-Young CHOI, Insup LEE, "Model Checking of Real-Time Properties of Resource-Bound Process Algebra" in IEICE TRANSACTIONS on Fundamentals,
vol. E92-A, no. 11, pp. 2781-2789, November 2009, doi: 10.1587/transfun.E92.A.2781.
Abstract: The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are difficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E92.A.2781/_p
Copiar
@ARTICLE{e92-a_11_2781,
author={Junkil PARK, Jungjae LEE, Jin-Young CHOI, Insup LEE, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Model Checking of Real-Time Properties of Resource-Bound Process Algebra},
year={2009},
volume={E92-A},
number={11},
pages={2781-2789},
abstract={The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are difficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.},
keywords={},
doi={10.1587/transfun.E92.A.2781},
ISSN={1745-1337},
month={November},}
Copiar
TY - JOUR
TI - Model Checking of Real-Time Properties of Resource-Bound Process Algebra
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2781
EP - 2789
AU - Junkil PARK
AU - Jungjae LEE
AU - Jin-Young CHOI
AU - Insup LEE
PY - 2009
DO - 10.1587/transfun.E92.A.2781
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E92-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 2009
AB - The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are difficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.
ER -