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 1 |
Fingerprint
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 journal › Article
}
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 -