Model Checking of Real-Time Properties of Resource-Bound Process Algebra
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Park, Junkil | - |
dc.contributor.author | Lee, Jungjae | - |
dc.contributor.author | Choi, Jin-Young | - |
dc.contributor.author | Lee, Insup | - |
dc.date.accessioned | 2021-09-08T12:00:22Z | - |
dc.date.available | 2021-09-08T12:00:22Z | - |
dc.date.created | 2021-06-11 | - |
dc.date.issued | 2009-11 | - |
dc.identifier.issn | 0916-8508 | - |
dc.identifier.uri | https://scholar.korea.ac.kr/handle/2021.sw.korea/119005 | - |
dc.description.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. | - |
dc.language | English | - |
dc.language.iso | en | - |
dc.publisher | IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG | - |
dc.subject | VERIFICATION | - |
dc.title | Model Checking of Real-Time Properties of Resource-Bound Process Algebra | - |
dc.type | Article | - |
dc.contributor.affiliatedAuthor | Choi, Jin-Young | - |
dc.identifier.doi | 10.1587/transfun.E92.A.2781 | - |
dc.identifier.scopusid | 2-s2.0-84867382516 | - |
dc.identifier.wosid | 000272773700017 | - |
dc.identifier.bibliographicCitation | IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, v.E92A, no.11, pp.2781 - 2789 | - |
dc.relation.isPartOf | IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES | - |
dc.citation.title | IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES | - |
dc.citation.volume | E92A | - |
dc.citation.number | 11 | - |
dc.citation.startPage | 2781 | - |
dc.citation.endPage | 2789 | - |
dc.type.rims | ART | - |
dc.type.docType | Article | - |
dc.description.journalClass | 1 | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
dc.relation.journalResearchArea | Engineering | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Hardware & Architecture | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Information Systems | - |
dc.relation.journalWebOfScienceCategory | Engineering, Electrical & Electronic | - |
dc.subject.keywordPlus | VERIFICATION | - |
dc.subject.keywordAuthor | ACSR | - |
dc.subject.keywordAuthor | model checking | - |
dc.subject.keywordAuthor | action-based modeling | - |
dc.subject.keywordAuthor | real-time temporal logic | - |
dc.subject.keywordAuthor | resource-bound process algebra | - |
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
(02841) 서울특별시 성북구 안암로 14502-3290-1114
COPYRIGHT © 2021 Korea University. All Rights Reserved.
Certain data included herein are derived from the © Web of Science of Clarivate Analytics. All rights reserved.
You may not copy or re-distribute this material in whole or in part without the prior written consent of Clarivate Analytics.