- Award ID(s):
- 1828811
- NSF-PAR ID:
- 10094356
- Date Published:
- Journal Name:
- SPIE Artificial Intelligence and Machine Learning for Multi-Domain Operations Applications
- Page Range / eLocation ID:
- 60
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
Traffic congestion and accidents are increasing exponentially worldwide. More vehicles are sold every year which leads to more traffic fatalities and congestion. There have been several efforts worldwide for mobile Cyber Physical Systems (CPS) to address a range of problems including traffic congestion, accidents, unnecessary time spent in traffic jams, and overall infotainment by using onboard communicating and computing technologies. However, when we use peer-to-peer network-based communication for mobile CPS, malicious users/vehicles could mislead the mobile CPS by not reporting their true periodic status data to their neighbors on the road. In this paper, we study a data validation and correction approach for resiliency in mobile CPS that uses a diverse set of data for reducing false information. Numerical results obtained from Monte Carlo simulation are used to evaluate the proposed approach. Results show that the proposed approach minimizes the false data in the mobile CPS to enhance the resiliency.more » « less
-
ABSTRACT: This paper explores the use of cyber-physical systems (CPS) for optimal design in wind engineering. The approach combines the accuracy of physical wind tunnel testing with the ability to efficiently explore a solution space using numerical optimization algorithms. The approach is fully automated, with experiments executed in a boundary layer wind tunnel (BLWT), sensor feedback monitored by a high-performance computer, and actuators used to bring about physical changes in the BLWT. Because the model is undergoing physical change as it approaches the optimal solution, this approach is given the name “loop-in-the-model” testing. The building selected for this study is a low-rise structure with a parapet wall of variable height. Parapet walls alter the location of the roof corner vortices, alleviating large suction loads on the windward facing roof corner and edges and setting up an interesting optimal design problem. In the BLWT, the model parapet height is adjusted using servo-motors to achieve a particular design. The model surface is instrumented with pressure taps to measure the envelope pressure loading. The taps are densely spaced on the roof to provide sufficient resolution to capture the change in roof corner vortex formation. Experiments are conducted using a boundary BLWT located at the University of Florida Natural Hazard Engineering Research Infrastructure (NHERI) Experimental Facility. The proposed CPS approach enables the optimal solution to be found quicker than brute force methods, in particular for complex structures with many design variables. The parapet wall provides a proof-of-concept study with a single design variable that has a non-monotonic influence on a structure’s wind load. This study focuses on envelope load effects, seeking the parapet height that minimizes roof and parapet wall suction loading. Implications are significant for more complex structures where the optimal solution may not be obvious and cannot be reasonably determined with traditional experimental or computational methods. KEYWORDS: Cyber-physical systems, optimization, boundary-layer wind tunnel, parapet wall, NHERImore » « less
-
Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived
automatically from its implementation. Our approach requires that the system implementation is specified inLingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5 using theZ3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifier correctly checks 21 out of 22 programs automatically. -
Systems for Internet of Things (IoT) have generated new requirements in all aspects of their development and deployment, including expanded Quality of Service (QoS) needs, enhanced resiliency of computing and connectivity, and the scalability to support massive numbers of end devices in a variety of applications. The research reported here concerns the development of a reliable and secure IoT/cyber physical system (CPS), providing network support for smart and connected communities, to be realized by means of distributed, secure, resilient Edge Cloud (EC) computing. This distributed EC system will be a network of geographically distributed EC nodes, brokering between end-devices and Backend Cloud (BC) servers. This paper focuses on three main aspects of the CPS: a) resource management in mobile cloud computing; b) information management in dynamic distributed databases; and c) biological-inspired intrusion detection system.more » « less
-
Industries are embracing information technology and constructing more robust machines known as Cyber-Physical Systems(CPS) to automate processes. CPSs are envisioned to be pervasive, coordinating, and integrating computation, sensing, actuation, and physical processes. CPSs have various applications in life-critical scenarios, where their performance and reliability can have direct impacts on human safety and well-being. However, CPSs are vulnerable to malicious attacks, and researchers have developed detectors to identify such attacks in different contexts. Surprisingly, little work has been done to detect attacks on the actuators of CPS. Furthermore, actuators face a high risk of optimal hidden attacks designed by powerful attackers, which can push them into an unsafe state without detection. To the best of our knowledge, no such attacks on actuators have been developed yet. In this paper, we design an optimal hidden attack for actuators and evaluate its effectiveness. First, we develop a mathematical model for actuators and then create a linear program for convex optimization. Second, we solve the optimization problem and simulate the optimal attack.more » « less