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 language | English |
|---|---|
| Pages (from-to) | 2781-2789 |
| Number of pages | 9 |
| Journal | IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences |
| Volume | E92-A |
| Issue number | 11 |
| DOIs | |
| Publication status | Published - 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
Park, J., Lee, J., Choi, J. Y., & Lee, I. (2009). Model checking of real-time properties of resource-bound process algebra. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, E92-A(11), 2781-2789. https://doi.org/10.1587/transfun.E92.A.2781