An official website of the United States government
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
Deciding Branching Hyperproperties for Real Time Systems
Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula ℑ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon T. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval.
more »
« less
- Award ID(s):
- 1900924
- PAR ID:
- 10559319
- Publisher / Repository:
- IEEE 37th Computer Security Foundations Symposium (CSF)
- Date Published:
- ISBN:
- 979-8-3503-6203-9
- Page Range / eLocation ID:
- 65 to 79
- Format(s):
- Medium: X
- Location:
- Enschede, Netherlands
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We consider the verification of input-relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations, monotonicity, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. We introduce a novel concept of difference tracking to compute the difference between the outputs of two executions of the same DNN at all layers. We design a new abstract domain, DiffPoly for efficient difference tracking that can scale large DNNs. DiffPoly is equipped with custom abstract transformers for common activation functions (ReLU, Tanh, Sigmoid, etc.) and affine layers and can create precise linear cross-execution constraints. We implement an input-relational verifier for DNNs called RaVeN which uses DiffPoly and linear program formulations to handle a wide range of input-relational properties. Our experimental results on challenging benchmarks show that by leveraging precise linear constraints defined over multiple executions of the DNN, RaVeN gains substantial precision over baselines on a wide range of datasets, networks, and input-relational properties.more » « less
-
null (Ed.)Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring — such as the realizability of all truth values — can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.more » « 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 derivedautomaticallyfrom 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 engineUclid5using theZ3SMT 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 Verifierand 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 Verifiercorrectly checks 21 out of 22 programs automatically.more » « less
-
null (Ed.)Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a generalized Büchi automaton of size 5^|φ| where |φ| denotes the length of an rLTL formula φ. It was recently shown that the size of this automaton can be reduced to 3^|φ| (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduce Evrostos, the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the aforementioned fragment incurs in a time overhead that makes the verification of rLTL practical.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/CSF61375.2024.00032
