An official website of the United States government
This paper introduces Shelley, a novel model checking framework used to verify the order of function calls, developed in the context of Cyber-Physical Systems (CPS). Shelley infers the model directly from MicroPython code, so as to simplify the process of checking requirements expressed in a temporal logic. Applications for CPS need to reason about the end of execution to verify the reclamation/release of physical resources, so our temporal logic is stated on finite traces. Lastly, Shelley infers the behavior from code using an inter-procedural and compositional analysis, thus supporting the usual object-oriented programming techniques employed in MicroPython code. To evaluate our work, we present an experience report on an industrial application and evaluate the bounds of the validity checks (up to subsystems under 10 s on a desktop computer).
more »
« less
Poster Abstract: Assuring LLM-Enabled Cyber-Physical Systems
Cyber-Physical Systems (CPS) are integrations of computation, networking, and physical processes. The autonomy and self-adaptation capabilities of CPS mark a significant evolution from traditional control systems. Machine learning significantly enhances the functionality and efficiency of Cyber-Physical Systems (CPS). Large Language Models (LLM), like GPT-4, can augment CPS’s functionality to a new level by providing advanced intelligence support. This fact makes the applications above potentially unsafe and thus untrustworthy if deployed to the real world. We propose a comprehensive and general assurance framework for LLM-enabled CPS. The framework consists of three modules: (i) the context grounding module assures the task context has been accurately grounded (ii) the temporal Logic requirements specification module forms the temporal requirements into logic specifications for prompting and further verification (iii) the formal verification module verifies the output of the LLM and provides feedback as a guideline for LLM. The three modules execute iteratively until the output of LLM is verified. Experiment results demonstrate that our assurance framework can assure the LLM-enabled CPS.
more »
« less
- Award ID(s):
- 2333980
- PAR ID:
- 10499419
- Publisher / Repository:
- ACM/IEEE
- Date Published:
- Journal Name:
- ACM/IEEE International Conference on Cyber-Physical Systems
- Format(s):
- Medium: X
- Location:
- Hong Kong, China
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Cyber-Physical Systems (CPS) integrate computational elements with physical processes via sensors and actuators. While CPS is expected to have human-level intelligence, traditional machine learning which is trained on specific and isolated datasets seems insufficient to meet such expectation. In recent years, Large Language Models (LLMs), like GPT-4, have experienced explosive growth and show significant improvement in reasoning and language comprehension capabilities which promotes LLM-enabled CPS. In this paper, we present a comprehensive review of these studies about LLM-enabled CPS. First, we overview LLM-enabled CPS and the roles that LLM plays in CPS. Second, we categorize existing works in terms of the application domain and discuss their key contributions. Third, we present commonly-used metrics and benchmarks for LLM-enabled CPS evaluation. Finally, we discuss future research opportunities and corresponding challenges of LLM-enabled CPS.more » « less
-
We present algorithms for Cyber-Physical Systems (CPS) falsification and control, which take advantage of knowing the entire language of the temporal logic specification - that is, the set of signals that satisfy the formula. In the design of CPS, falsification and control play key roles. Falsification is a testing task, where the goal is to find an input signal that causes the system's output trajectory to violate the correctness requirements. Control is the dual task, where the goal is to find an input signal that causes the system's output to satisfy the specification. When the specification is expressed in a temporal logic, most existing work relies on local optimization heuristics to perform both tasks. In this paper, we explore whether a different expression of the specification offers advantages when performing falsification and control. Recent work presented a method for computing a representation of the language of a formula in (discrete-time) Signal Temporal Logic (STL), showing that the language can be represented as a union of polytopes. We introduce new falsification algorithms which combine distance information to the different components of the language to accelerate the convergence to a falsifier. And we introduce a new algorithm for computing a satisfying control signal which works by repeatedly projecting violating output trajectories back onto the language's components. Moreover, these algorithms are trivially parallelizable to take advantage of multiple processors. Despite their relative simplicity, our algorithms demonstrate 10x to 100x speedups relative to the state-of-the-art.more » « less
-
In Cyber-Physical Systems (CPS), sensor data integrity is crucial since acting on malicious sensor data can cause serious consequences, given the tight coupling between cyber components and physical systems. While extensive works focus on sensor attack detection, attack diagnosis that aims to find out when the attack starts has not been well studied yet. This temporal sensor attack diagnosis problem is equally important because many recovery methods rely on the accurate determination of trustworthy historical data. To address this problem, we propose a lightweight data-driven solution to achieve real-time sensor attack diagnosis. Our novel solution consists of five modules, with the attention and diagnosis ones as the core. The attention module not only helps accurately predict future sensor measurements but also computes statistical attention scores for the diagnosis module. Based on our unique observation that the score fluctuates sharply once an attack launches, the diagnosis module determines the onset of an attack through monitoring the fluctuation. Evaluated on high-dimensional high-fidelity simulators and a testbed, our solution demonstrates robust and accurate temporal diagnosis results while incurring millisecond-level computational overhead on Raspberry Pi.more » « less
-
Modern cyber-physical systems-of-systems (CPSoS) operate in complex systems-of-systems that must seamlessly work together to control safety- or mission-critical functions. Linear Temporal Logic (LTL) and Mission-time Linear Temporal logic (MLTL) intuitively express CPSoS requirements for automated system verification and validation. However, both LTL and MLTL presume that all signals populating the variables in a formula are sampled over the same rate and type (e.g., time or distance), and agree on a standard “time” step. Formal verification of cyber-physical systems-of-systems needs validate-able requirements expressed over (sub-)system signals of different types, such as signals sampled at different timescales, distances, or levels of abstraction, expressed in the same formula. Previous works developed more expressive logics to account for types (e.g., timescales) by sacrificing the intuitive simplicity of LTL. However, a legible direct one-to-one correspondence between a verbal and formal specification will ease validation, reduce bugs, increase productivity, and linearize the workflow from a project’s conception to actualization. Validation includes both transparency for human interpretation, and tractability for automated reasoning, as CPSoS often run on resource-limited embedded systems. To address these challenges, we introduced Mission-time Linear Temporal Logic Multi-type (Hariharan et al., Numerical Software Verification Workshop, 2022), a logic building on MLTL. MLTLM enables writing formal requirements over finite input signals (e.g., sensor signals and local computations) of different types, while maintaining the same simplicity as LTL and MLTL. Furthermore, MLTLM maintains a direct correspondence between a verbal requirement and its corresponding formal specification. Additionally, reasoning a formal specification in the intended type (e.g., hourly for an hourly rate, and per second for a seconds rate) will use significantly less memory in resource-constrained hardware. This article extends the previous work with (1) many illustrated examples on types (e.g., time and space) expressed in the same specification, (2) proofs omitted for space in the workshop version, (3) proofs of succinctness of MLTLM compared to MLTL, and (4) a minimal translation to MLTL of optimal length.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Proceeding:
- The DOI is not currently available.
