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