Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification’s reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28
This paper presents a compositional approach to modelbased test derivation in Behavior-Driven Development (BDD). In BDD, system behavior is specified through scenarios written in natural language. For each scenario, a test case can be derived. However, such test cases do not cover the integration of multiple behaviors, while that is where potential faults may very well occur. To counter this, we introduce a formal composition operator for sequential composition, which integrates the individual BDDs while preserving their test coverage. We also report on a prototype tool that integrates model-based features into an existing testing framework that supports BDD-based test derivation. We show the feasibility and advantages of our approach by applying the prototype to a real-world case study.
Secure multiparty computation (hereafter, SMC) refers to cryptographic protocols that allow multiple parties to jointly compute a function over their inputs while keeping them private. The main security property of SMC protocols is information leakage freedom, whose proofs can be found in the scientific literature for idealized models. But how does one guarantee that information leakage freedom still holds once SMC is implemented as a concrete piece of software? As a step toward solving this problem, we use the proof assistant Rocq to formalize the security claims of an SMC stack. We develop a method based on an interpreter for a subset of the π -calculus in which protocols can be modeled as programs and then input traces verified for correctness and information leakage freedom. Thanks to this approach, the properties of SMC can be established in a clearly defined trusted base that can be reused to verify other SMC stacks.
Noninterference theory aims at ensuring the absence of covert channels among different security levels. As far as the verification of information-flow properties via equivalence checking is concerned, in nondeterministic and probabilistic settings weak bisimilarity has turned out to be adequate only for standard systems, while branching bisimilarity has proven to be appropriate for reversible systems too. In this paper we investigate noninterference for stochastically timed systems represented in the interactive Markov chain model of Hermanns. After recasting a selection of noninterference properties via Markovian variants of weak and branching bisimilarities, we study their preservation and compositionality aspects, build their taxonomy, and compare it with the nondeterministic and probabilistic taxonomies. We show the adequacy of our proposal through some examples about a database management system.
Testing connected cyber-physical systems (CPS) is a complex task. Connected CPS feature complex stochastic dynamic behaviour in interaction with the physical and human environment as well as communication over networks. Devising an oracle for testing connected CPS is a challenge; the oracle should be able to quantitatively reason about the stochastic nature of the interactions between the CPS and its environment. The quantitative reasoning should be sensitive to significant deviations in the dynamics and neglect minor deviations, e.g., due to measurement errors. To address this challenge, we provide the mathematical framework for conformance testing of connected CPS. We define a quantitative measure of closeness for two distributions of trajectories (i.e., output distributions from two distinct stochastic systems that are provided with the same input stimuli) that allows for capturing significant temporal and spatial deviations and neglecting subtle ones. This measure forms the basis for our notion of stochastic conformance, which determines when two stochastic systems conform to each other. We implement our proposed notion of stochastic conformance and compare our notion against a state-of-the-art baseline by applying both approaches to a case study involving a platoon of connected vehicles. Our notion detects a variety of different types of faults whilst allowing subtle deviations resulting from naturally occurring perturbations inherent to CPS.
