The search functionality is under construction.

The search functionality is under construction.

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

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.

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 -