IEICE TRANSACTIONS on Fundamentals
Model Checking of Real-Time Properties of Resource-Bound Process Algebra
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E92-A No.11 pp.2781-2789
- Publication Date
- 2009/11/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1587/transfun.E92.A.2781
- Type of Manuscript
- Special Section PAPER (Special Section on Theory of Concurrent Systems and its Applications)
- Category
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
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
Copy
@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},}
Copy
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 -
English
