scholarly journals Deriving Specifications of Control Programs for Cyber Physical Systems

2019 ◽  
Vol 63 (5) ◽  
pp. 774-790
Author(s):  
Alan Burns ◽  
Ian J Hayes ◽  
Cliff B Jones
Keyword(s):  
Physical Environment ◽  
Control Program ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Control Programs ◽  
Use Of Time ◽  
Temporal Properties ◽  
Physical Components

Abstract Cyber physical systems (CPS) exist in a physical environment and comprise both physical components and a control program. Physical components are inherently liable to failure and yet an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes a framework for deriving the specification of the software control component of a CPS from an understanding of the behaviour required of the overall system in its physical environment. The two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to allow specifications to be obtained systematically from requirements (as expressed in terms of the required behaviour in the environment) and nested assumptions (about the physical components of the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at a number of different granularities. The key contribution is in combining these ideas; using time bands overcomes a significant drawback in earlier work. The paper also addresses the means by which the reliability of a CPS can be addressed by challenging each rely condition in the derived specification and, where appropriate, improve robustness and/or define weaker guarantees that can be delivered with respect to the corresponding weaker rely conditions.

scholarly journals A spatio-temporal specification language and its completeness & decidability

2020 ◽  
Vol 9 (1) ◽  
Author(s):  
Tengfei Li ◽  
Jing Liu ◽  
Haiying Sun ◽  
Xiang Chen ◽  
Lipeng Zhang ◽  
...  
Keyword(s):  
Intelligent Transportation System ◽  
Cyber Physical Systems ◽  
Specification Language ◽  
Finite Model ◽  
Critical Systems ◽  
Physical Systems ◽  
Spatial Objects ◽  
Temporal Properties ◽  
Spatio Temporal ◽  
Temporal Specification

AbstractIn the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL PC and analyze the complexity of STSL PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL OC, and provide the proof of its axiomatization system and decidability.

A Model-Based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems

2016 ◽  
Vol 13 (1) ◽  
pp. 40-52 ◽  
Author(s):  
Peter Herrmann ◽  
Jan Olaf Blech ◽  
Fenglin Han ◽  
Heinz Schmidt
Keyword(s):  
Real Time ◽  
Physical Environment ◽  
Spatial Model ◽  
Physical Space ◽  
Cyber Physical Systems ◽  
Spatial Behavior ◽  
Model Checker ◽  
Control Software ◽  
Physical Systems ◽  
Model Based

A method preserving cyber-physical systems to operate safely in a joint physical space is presented. It comprises the model-based development of the control software and simulators for the continuous physical environment as well as proving the models for spatial and real-time properties. The corresponding toolchain is based on the model-based engineering tool Reactive Blocks and the spatial model checker BeSpaceD. The real-time constraints to be kept by the controller are proven using the model checker UPPAAL.

scholarly journals Hybrid SynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL

2021 ◽  
pp. 491-504
Author(s):  
Jaehun Lee ◽  
Sharon Kim ◽  
Kyungmin Bae ◽  
Peter Csaba Ölveczky
Keyword(s):  
Formal Analysis ◽  
Cyber Physical Systems ◽  
Modeling Language ◽  
Analysis Tool ◽  
Physical Systems ◽  
Complex Control ◽  
Control Programs ◽  
Network Delays ◽  
Execution Times

AbstractWe present the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs. We define the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL on a number of applications.

scholarly journals Quality control in cyber-physical systems of smart electronics manufacturing

2021 ◽  
Vol 2094 (4) ◽  
pp. 042066
Author(s):  
A A Dzyubanenko ◽  
G I Korshunov
Keyword(s):  
Physical Environment ◽  
Printed Circuit Boards ◽  
Cyber Physical Systems ◽  
Problem Area ◽  
Smart Manufacturing ◽  
High Tech ◽  
Circuit Boards ◽  
Physical Systems ◽  
Printed Circuit ◽  
Surface Mounting

Abstract The creation of high-tech smart industries is observed in dynamically developing industries, which include the production of electronics and the automotive industry. The concept of “smart manufacturing” is closely related to the concept of cyber-physical systems, which integrates the main elements of digitalization and intellectualization. This concept provides for the continuous improvement of intellectual “cybernetic” resources for the effective management of the “physical” environment considered in this problem area. Improvement of technologies, ensuring high rates of reproducibility and suitability of equipment creates conditions for defect-free production. However, there remain the problems of recognizing patterns represented not by an obvious marriage, but by some not fully defined inconsistency on a set of requirements. The need to disclose uncertainties of this kind is typical for surface mounting technologies for printed circuit boards. The introduction of more and more advanced automatic optical inspections, containing the possibility of introducing intelligent (cybernetic) means, creates conditions for improving the quality of printed circuit boards as a “physical” environment. It is also important to minimize the “human factor”, the presence of which is still used when making decisions on the results of control. In the article, ensuring the rhythm of digital production and increasing the reliability of control in quality management in smart high-tech industries using the example of electronics production.

HIGH FIDELITY VIRTUALIZATION OF CYBER-PHYSICAL SYSTEMS

2013 ◽  
Vol 04 (02) ◽  
pp. 1340005 ◽  
Author(s):  
YU ZHANG ◽  
FEI XIE ◽  
YUNWEI DONG ◽  
GANG YANG ◽  
XINGSHE ZHOU
Keyword(s):  
Control Systems ◽  
Virtual Machine ◽  
Complete System ◽  
Cyber Physical Systems ◽  
High Fidelity ◽  
Physical Systems ◽  
Early Exploration ◽  
Continuous Domains ◽  
Execution Environment ◽  
Physical Components

Cyber-physical systems (CPS) tightly integrate cyber and physical components and transcend discrete and continuous domains. It is greatly desired that the synergy between cyber and physical components of CPS is explored even before the complete system is put together. Virtualization has potential to play a significant role in exploring such synergy. In this paper, we propose a CPS virtualization approach based on the integration of virtual machine and physical component emulator. It enables real software, virtual hardware, and virtual physical components to execute in a holistic virtual execution environment. We have implemented this approach using QEMU as the virtual machine and Matlab/Simulink as the physical component emulator, respectively. To achieve high-fidelity between the real system and its virtualization, we have developed a strategy for synchronizing the virtual machine and the physical component emulator. To evaluate our approach, we have successfully applied it to real-world control systems. Experiments results have shown that our approach achieves high-fidelity in capturing dynamic behaviors of the entire system. This approach is promising in enabling early development of cyber components of CPS and early exploration of the synergy of cyber and physical components.

scholarly journals Cyber-Physical Systems: A Literature Review

2017 ◽  
Vol 13 (36) ◽  
pp. 52 ◽  
Author(s):  
Matthew N. O. Sadiku ◽  
Yonghui Wang ◽  
Suxia Cui ◽  
Sarhan M. Musa
Keyword(s):  
Information Processing ◽  
Embedded Systems ◽  
Literature Review ◽  
Virtual World ◽  
Daily Life ◽  
Physical World ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Smart Systems ◽  
Physical Components

Cyber-physical systems (CPSs) are smart systems that depend on the synergy of cyber and physical components. They link the physical world (e.g. through sensors, actuators, robotics, and embedded systems) with the virtual world of information processing. Applications of CPS have the tremendous potential of improving convenience, comfort, and safety in our daily life. This paper provides a brief introduction to CPSs and their applications.

scholarly journals A model-based software development method for automotive cyber-physical systems

2011 ◽  
Vol 8 (4) ◽  
pp. 1277-1301 ◽  
Author(s):  
Zhigang Gao ◽  
Haixia Xia ◽  
Guojun Dai
Keyword(s):  
Software Development ◽  
Code Generation ◽  
Physical Environment ◽  
Source Code ◽  
Cyber Physical Systems ◽  
Functional Requirements ◽  
Development Method ◽  
Physical Systems ◽  
Implementation Model ◽  
Model Based

The development of automotive cyber-physical systems (CPS) software needs to consider not only functional requirements, but also non-functional requirements and the interaction with physical environment. In this paper, a model-based software development method for automotive CPS (MoBDAC) is presented. The main contributions of this paper are threefold. First, MoBDAC covers the whole development workflow of automotive CPS software from modeling and simulation to code generation. Automatic tools are used to improve the development efficiency. Second, MoBDAC extracts nonfunctional requirements and deals with them in the implementation model level and source code level, which helps to correctly manage and meet non-functional requirements. Third, MoBDAC defines three kinds of relations between uncertain physical environment events and software internal actions in automotive CPS, and uses Model Modifier to integrate the interaction with physical environment. Moreover, we illustrate the development workflow of MoBDAC by an example of a power window development.

Butterfly Attack: Adversarial Manipulation of Temporal Properties of Cyber-Physical Systems

2019 ◽  
Author(s):  
Rouhollah Mahfouzi ◽  
Amir Aminifar ◽  
Soheil Samii ◽  
Mathias Payer ◽  
Petru Eles ◽  
...  
Keyword(s):  
Cyber Physical Systems ◽  
Physical Systems ◽  
Temporal Properties

scholarly journals A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems

2022 ◽  
Vol Volume 18, Issue 1 ◽  
Author(s):  
L. Nenzi ◽  
E. Bartocci ◽  
L. Bortolussi ◽  
M. Loreti
Keyword(s):  
Ad Hoc ◽  
Dynamic Networks ◽  
Physical Space ◽  
Weighted Graph ◽  
Cyber Physical Systems ◽  
Dynamic Interactions ◽  
Physical Systems ◽  
Temporal Properties ◽  
Spatially Distributed ◽  
Spatio Temporal

Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19.

Sign in / Sign up

Export Citation Format

Share Document