Open Access System for Information Sharing

Login Library

 

Article
Cited 21 time in webofscience Cited 24 time in scopus
Metadata Downloads

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study SCIE SCOPUS

Title
Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study
Authors
Bae, KKrisiloff, JMeseguer, JOumllveczky, PC
Date Issued
2015-06-01
Publisher
Elsevier
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.
URI
https://oasis.postech.ac.kr/handle/2014.oak/36399
DOI
10.1016/J.SCICO.2014.09.011
ISSN
0167-6423
Article Type
Article
Citation
SCIENCE OF COMPUTER PROGRAMMING, vol. 103, page. 13 - 50, 2015-06-01
Files in This Item:
There are no files associated with this item.

qr_code

  • mendeley

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Related Researcher

Researcher

배경민BAE, KYUNGMIN
Dept of Computer Science & Enginrg
Read more

Views & Downloads

Browse