Model Checking of Real-Time Properties of Resource-Bound Process Algebra
- Authors
- Park, Junkil; Lee, Jungjae; Choi, Jin-Young; Lee, Insup
- Issue Date
- 11월-2009
- Publisher
- IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG
- Keywords
- ACSR; model checking; action-based modeling; real-time temporal logic; resource-bound process algebra
- Citation
- IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, v.E92A, no.11, pp.2781 - 2789
- Indexed
- SCIE
SCOPUS
- Journal Title
- IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES
- Volume
- E92A
- Number
- 11
- Start Page
- 2781
- End Page
- 2789
- URI
- https://scholar.korea.ac.kr/handle/2021.sw.korea/119005
- DOI
- 10.1587/transfun.E92.A.2781
- ISSN
- 0916-8508
- 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 difficult 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.
- Files in This Item
- There are no files associated with this item.
- Appears in
Collections - School of Cyber Security > Department of Information Security > 1. Journal Articles
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.