Model Checking of Real-Time Properties of Resource-Bound Process Algebra

Junkil PARK; Jungjae LEE; Jin-Young CHOI; Insup LEE

doi:10.1587/transfun.E92.A.2781

Model Checking of Real-Time Properties of Resource-Bound Process Algebra

Junkil PARK, Jungjae LEE, Jin-Young CHOI, Insup LEE

Full Text Views

0

Cite this

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

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 -