This work presents a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre, and contributes an interactive visualiser that renders a property's three-valued verdict over an editable trace.
Abstract
Signal Temporal Logic (STL) is a popular formalism for the temporal safety properties of cyber-physical systems, most often used for runtime verification. In the synchronous family of languages, safety properties are instead expressed as synchronous observers, modules composed with a program for static verification, which are also runnable specifications suitable for runtime verification, though this use is rarely explored. We present a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre. Unlike previous work, we allow arbitrary nesting of bounded SSTL properties via modular compilation, and admit a globally unbounded outer operator for online monitoring; the resulting observers serve both runtime verification and, as a by-product, static verification with the Kind2 model checker. We further contribute an interactive visualiser that renders a property's three-valued verdict over an editable trace, and evaluate on two case studies from the literature: a spring-mass system and a car-following cruise controller.
This work presents a lightweight and modular proof technique for verifying eventual progression guarantees for Rust async runtimes and realizes this proof technique as a set of static analyses for Rust and uses these to verify eventual progression of several key components of multiple Rust async runtime implementations...
Yan-Ze Li, Ivan Beschastnikh, Alexander J. Summers· 0 citations
This work introduces an append-only logical event log that abstracts implementation details and enables a Kamp-style translation of Linear Temporal Logic into First-Order Logic, which enables deductive program verifiers to reason about progress via monotonic timestamps without needing native temporal logic support.
Ti Zhou, Zi-Hao Zhang, Omar Chowdhury et al.· Proceedings of the ACM SIGOP...· 1 citation
Formal specification techniques have been introduced to address the ambiguities inherent in natural-language hardware specifications. One such approach is the Universal Specification Format (USF), which provides a machine-readable, formal reference for Register-Transfer Level (RTL) verification. However, verifying agai...
Robert Kunzelmann, Raphael Kunz, Stephanie Ecker et al.· Journal of Signal Processing...· 0 citations
Formal methods, including model checking, are rapidly gaining importance, especially in safety-critical domains like aerospace and automotive. Consequently, the systems to be verified are growing more complex and are described in diverse design languages, often expressive and ambiguous. However, model checkers oper...
Zsófia Ádám, Zoltán Micskei· Journal of Software and Syst...· 0 citations
Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system's behaviour can be observed. For some properties, these fini...
Rayhana Amjad, R. V. van Glabbeek, Liam O'Connor· Information and Computation· 0 citations
When safety-critical systems are developed from a known internal specification, their correctness can be established by model checking. In the frequent case where such a specification is unknown or inaccessible, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic syst...
Sarah Winkler, Toryn Q. Klassen, Sheila A. McIlraith et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
