DC Field | Value | Language |
---|---|---|
dc.contributor.author | Bae, K | - |
dc.contributor.author | Krisiloff, J | - |
dc.contributor.author | Meseguer, J | - |
dc.contributor.author | Ouml | - |
dc.contributor.author | lveczky, PC | - |
dc.date.accessioned | 2017-07-19T12:45:51Z | - |
dc.date.available | 2017-07-19T12:45:51Z | - |
dc.date.created | 2016-02-24 | - |
dc.date.issued | 2015-06-01 | - |
dc.identifier.issn | 0167-6423 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/36399 | - |
dc.description.abstract | Distributed cyber-physical systems (DCPS), such as aeronautics and ground transportation systems, are very hard to design and verify, because of asynchronous communication, network delays, and clock skews. Their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system's concurrency. The Multirate PALS ("physically asynchronous, logically synchronous") methodology has been proposed to reduce the design and verification of a DCPS to the much simpler task of designing and verifying its underlying synchronous version, where components may operate with different periods. This paper presents a methodology for formally modeling and verifying multirate DCPSs using Multirate PALS. In particular, this methodology explains how to deal with the system's physical environment in Multirate PALS. We illustrate our methodology with a multirate DCPS consisting of an airplane maneuvered by a pilot, who turns the airplane to a specified angle through a distributed control system. Our formal analysis using Real-Time Maude revealed that the original design did not achieve a smooth turning maneuver, and led to a redesign of the system. We then use model checking and Multirate PALS to prove that the redesigned system satisfies the desired correctness properties, whereas model checking the corresponding asynchronous model is unfeasible. This shows that Multirate PALS is not only effective for formal DCPS verification, but can also be used effectively in the DCPS design process. (C) 2014 Elsevier B.V. All rights reserved. | - |
dc.language | English | - |
dc.publisher | Elsevier | - |
dc.relation.isPartOf | SCIENCE OF COMPUTER PROGRAMMING | - |
dc.title | Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study | - |
dc.type | Article | - |
dc.identifier.doi | 10.1016/J.SCICO.2014.09.011 | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | SCIENCE OF COMPUTER PROGRAMMING, v.103, pp.13 - 50 | - |
dc.identifier.wosid | 000351964100003 | - |
dc.date.tcdate | 2019-02-01 | - |
dc.citation.endPage | 50 | - |
dc.citation.startPage | 13 | - |
dc.citation.title | SCIENCE OF COMPUTER PROGRAMMING | - |
dc.citation.volume | 103 | - |
dc.contributor.affiliatedAuthor | Bae, K | - |
dc.identifier.scopusid | 2-s2.0-84924496519 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.wostc | 14 | - |
dc.description.scptc | 15 | * |
dc.date.scptcdate | 2018-05-121 | * |
dc.type.docType | Article; Proceedings Paper | - |
dc.subject.keywordPlus | REAL-TIME | - |
dc.subject.keywordPlus | SPECIFICATION | - |
dc.subject.keywordPlus | PATTERN | - |
dc.subject.keywordAuthor | Multirate PALS | - |
dc.subject.keywordAuthor | Cyber-physical systems | - |
dc.subject.keywordAuthor | Real-Time Maude | - |
dc.subject.keywordAuthor | Model checking | - |
dc.subject.keywordAuthor | Hybrid systems | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.