Model checking of real-time properties of resource-bound process algebra

Junkil Park, Jungjae Lee, Jin Young Choi, Insup Lee

Research output: Contribution to journalArticle

1 Citation (Scopus)

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 di fficult 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.

Original languageEnglish
Pages (from-to)2781-2789
Number of pages9
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
VolumeE92-A
Issue number11
DOIs
Publication statusPublished - 2009 Nov 1

Fingerprint

Process Algebra
Model checking
Algebra
Model Checking
Real-time
Resources
Bisimulation
Temporal Logic
Temporal logic
Complex Systems
Large scale systems
Model
Logic
Verify
Requirements
Demonstrate

Keywords

  • ACSR
  • Action-based modeling
  • Model checking
  • Real-time temporal logic
  • Resource-bound process algebra

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Computer Graphics and Computer-Aided Design
  • Applied Mathematics
  • Signal Processing

Cite this

Model checking of real-time properties of resource-bound process algebra. / Park, Junkil; Lee, Jungjae; Choi, Jin Young; Lee, Insup.

In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E92-A, No. 11, 01.11.2009, p. 2781-2789.

Research output: Contribution to journalArticle

@article{32eae5b8fce14536b55f6e1573cbfb61,
title = "Model checking of real-time properties of resource-bound process algebra",
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 di fficult 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 = "ACSR, Action-based modeling, Model checking, Real-time temporal logic, Resource-bound process algebra",
author = "Junkil Park and Jungjae Lee and Choi, {Jin Young} and Insup Lee",
year = "2009",
month = "11",
day = "1",
doi = "10.1587/transfun.E92.A.2781",
language = "English",
volume = "E92-A",
pages = "2781--2789",
journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
issn = "0916-8508",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "11",

}

TY - JOUR

T1 - Model checking of real-time properties of resource-bound process algebra

AU - Park, Junkil

AU - Lee, Jungjae

AU - Choi, Jin Young

AU - Lee, Insup

PY - 2009/11/1

Y1 - 2009/11/1

N2 - 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 di fficult 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.

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 di fficult 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.

KW - ACSR

KW - Action-based modeling

KW - Model checking

KW - Real-time temporal logic

KW - Resource-bound process algebra

UR - http://www.scopus.com/inward/record.url?scp=84867382516&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867382516&partnerID=8YFLogxK

U2 - 10.1587/transfun.E92.A.2781

DO - 10.1587/transfun.E92.A.2781

M3 - Article

AN - SCOPUS:84867382516

VL - E92-A

SP - 2781

EP - 2789

JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

SN - 0916-8508

IS - 11

ER -