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

Keywords

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

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Model checking of real-time properties of resource-bound process algebra'. Together they form a unique fingerprint.

  • Cite this