More Like this

1. An STL-Based Formulation of Resilience in Cyber-Physical Systems

   https://doi.org/10.1007/978-3-031-15839-1_7  

   Chen, Hongkai; Lin, Shan; Smolka, Scott A.; Paoletti, Nicola (August 2022, Formal Modeling and Analysis of Timed Systems)

   Bogomolov, Sergiy; Parker, David (Ed.)

   Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical Systems (CPS), and yet, to date, there is no widely agreed-upon formal treatment of CPS resiliency. We present an STL-based framework for reasoning about resiliency in CPS in which resiliency has a syntactic characterization in the form of an STL-based Resiliency Specification (SRS). Given an arbitrary STL formula φ, time bounds α and β, the SRS of φ, Rα,β (φ), is the STL formula ¬φU[0,α]G[0,β)φ, specifying that recovery from a violation of φ occur within time α (recoverability), and subsequently that φ be maintained for duration β (durability). These R-expressions, which are atoms in our SRS logic, can be combined using STL operators, allowing one to express composite resiliency specifications, e.g., multiple SRSs must hold simultaneously, or the system must eventually be resilient. We define a quantitative semantics for SRSs in the form of a Resilience Satisfaction Value (ReSV) function r and prove its soundness and completeness w.r.t. STL’s Boolean semantics. The r-value for Rα,β (φ) atoms is a singleton set containing a pair quantifying recoverability and durability. The r-value for a composite SRS formula results in a set of non-dominated recoverability-durability pairs, given that the ReSVs of subformulas might not be directly comparable (e.g., one subformula has superior durability but worse recoverability than another). To the best of our knowledge, this is the first multi-dimensional quantitative semantics for an STL-based logic. Two case studies demonstrate the practical utility of our approach. https://doi.org/10.1007/978-3-031-15839-1_7 

   more » « less
2. A run-time verification method with consideration of uncertainties for cyber–physical systems

   https://doi.org/10.1016/j.micpro.2023.104890  

   Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Derler, Patricia; Andrade, Hugo (September 2023, Microprocessors and Microsystems)

   Since many Cyber–Physical Systems (CPS) interact with the real world, they are safety- or mission- critical. Temporal specification languages like STL (Signal Temporal Logic) have been developed to capture the properties that built CPS must meet. However, the existing temporal logics/languages do not provide a natural way to express the tolerance with which the timing properties must be met. As a consequence of this, the specified properties may be vague, the ensuing CPS design may end up being over- or under-provisioned, and the validation of whether the built CPS meets the specified CPS properties may turn out to be erroneous. To address these issues, a run-time verification methodology is proposed, that allows users to explicitly specify the tolerance with which timing properties must be met. To ensure the correctness of measurement-based validation of a built CPS, this article: (i) proposes a test to determine if a given measurement system can validate the properties specified in TTL, and (ii) proposes a measurement-based testing methodology to provide one-sided guarantee that the built CPS meets the specified CPS properties. The guarantees are one-sided in the sense that when the measurement-based testing concludes that the properties are met, then they are guaranteed to be met (so not false positive). However, when the measurement-based testing concludes that the properties were not met, then they may have met (there can be false negative). In order to validate our claims, we built a model of flying paster (part of the printing press that swaps in a new roll of paper when the current roll is about to finish) using Arduino Mega 2560 and two Hansen brushed DC motors and specified the timing constraints among the various events in this system, along with the tolerances with which they should be met in TTL. We generated the testing logic and validated that we get no false positive, even though we encounter 4.04% false negative. The rate of false negatives can be reduced to be less than any arbitrary value by using more accurate measurement equipment. 

   more » « less
3. Clairvoyant Monitoring for Signal Temporal Logic

   https://doi.org/10.1007/978-3-030-57628-8_11  

   Qin, Xin; Deshmukh, Jyotirmoy V (July 2020, Formal Modeling and Analysis of Timed Systems)

   Bertrand, N.; null (Ed.)

   In this paper, we consider the problem of monitoring temporal patterns expressed in Signal Temporal Logic (STL) over time-series data in a clairvoyant fashion. Existing offline or online monitoring algorithms can only compute the satisfaction of a given STL formula on the time-series data that is available. We use off-the-shelf statistical time-series analysis techniques to fit available data to a model and use this model to forecast future signal values. We derive the joint probability distribution of predicted signal values and use this to compute the satisfaction probability of a given signal pattern over the prediction horizon. There are numerous potential applications of such prescient detection of temporal patterns. We demonstrate practicality of our approach on case studies in automated insulin delivery, unmanned aerial vehicles, and household power consumption data. 

   more » « less
4. Interval Signal Temporal Logic From Natural Inclusion Functions

   https://doi.org/10.1109/LCSYS.2023.3337744  

   Baird, Luke; Harapanahalli, Akash; Coogan, Samuel (January 2023, IEEE Control Systems Letters)

   We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (I-STL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the min and max functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to I-STL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate I-STL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates. 

   more » « less
5. Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems

   https://doi.org/10.1145/3477032  

   Ma, Meiyi; Stankovic, John; Bartocci, Ezio; Feng, Lu (October 2021, ACM Transactions on Embedded Computing Systems)

   Predictive monitoring—making predictions about future states and monitoring if the predicted states satisfy requirements—offers a promising paradigm in supporting the decision making of Cyber-Physical Systems (CPS). Existing works of predictive monitoring mostly focus on monitoring individual predictions rather than sequential predictions. We develop a novel approach for monitoring sequential predictions generated from Bayesian Recurrent Neural Networks (RNNs) that can capture the inherent uncertainty in CPS, drawing on insights from our study of real-world CPS datasets. We propose a new logic named Signal Temporal Logic with Uncertainty (STL-U) to monitor a flowpipe containing an infinite set of uncertain sequences predicted by Bayesian RNNs. We define STL-U strong and weak satisfaction semantics based on whether all or some sequences contained in a flowpipe satisfy the requirement. We also develop methods to compute the range of confidence levels under which a flowpipe is guaranteed to strongly (weakly) satisfy an STL-U formula. Furthermore, we develop novel criteria that leverage STL-U monitoring results to calibrate the uncertainty estimation in Bayesian RNNs. Finally, we evaluate the proposed approach via experiments with real-world CPS datasets and a simulated smart city case study, which show very encouraging results of STL-U based predictive monitoring approach outperforming baselines. 

   more » « less