Verification of Cyberphysical Systems

Marjan Sirjani, Edward A. Lee and Ehsan Khamespanah
Additional contact information
Marjan Sirjani: School of IDT, Mälardalen University, 722 20 Västerås, Sweden
Edward A. Lee: Department of EECS, University of California at Berkeley, Berkeley, CA 94720-1770, USA
Ehsan Khamespanah: Department of ECE, University of Tehran, Tehran 1961733114, Iran

Mathematics, 2020, vol. 8, issue 7, 1-20

Abstract: The value of verification of cyberphysical systems depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature and different timelines of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. We describe a logical-time-based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear.

Keywords: cyberphysical systems; verification; Lingua Franca; model checking; Rebeca (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2020
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/8/7/1068/pdf (application/pdf)
https://www.mdpi.com/2227-7390/8/7/1068/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:8:y:2020:i:7:p:1068-:d:379333

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().