This paper presents an offline safety analysis framework for neural controllers in model predictive control settings. Building on the insight that a (sensed) reference trajectory can be treated as a disturbance preview, our method constructs a non-adversarial controlled invariant set that both captures realistic operating conditions and includes the adversarial disturbance set. This formulation reduces safety checking to a collection of input–output constraints on the neural network. Leveraging a neural network verifier, our approach identifies counterexamples even when nominal performance matches that of a model predictive controller baseline. In a lane-keeping automated-driving case study, we falsify three neural controllers within minutes. We demonstrate that disturbance preview reduces false alarms in counterexample search and that the workflow scales to networks of practical size. Thus, the framework offers an effective rigorous safety certification of learned controllers in cyber-physical systems.

Ensuring the safety of automated driving vehicles is particularly challenging due to the wide range of their operating conditions. This paper introduces CoCoSaFe, a Co mpositional Co de-level formal Sa fety verification F ram e work for automated driving controllers. Unlike traditional verification methods, such as model-based analysis, counterexample detection by guided simulation, or runtime verification through online monitoring, our approach verifies controller implementations directly at code level in an offline setting. Compositional contracts and bounded model checking are employed to assess the implementation of subsystem controllers against invariant sets. For neural network-based controllers, we introduce a scalable three-step decomposition method that utilizes a neural network verifier. CoCoSaFe is applied to adaptive cruise and lane-keeping controllers, for which we derive formal specifications and analytical models of the desired longitudinal and lateral behaviors, amenable for decoupled invariant sets. Various types of traditional and neural network controllers are verified in the order of minutes, showcasing its broad applicability and effectiveness in ensuring behavioral safety of software for automated driving and similar cyber–physical systems.

Abstract The formal safety analysis of automated driving vehicles poses unique challenges due to their dynamic operating conditions and significant complexity. This paper presents a case study of applying formal safety verification to adaptive cruise controllers. Unlike the majority of existing verification approaches in the automotive domain, which only analyze (potentially imperfect) controller models, employ simulation to find counter-examples or use online monitors for runtime verification, our method verifies controllers at code level by utilizing bounded model checking. Verification is performed against an invariant set derived from formal specifications and an analytical model of the required behavior. For neural network controllers, we propose a scalable three-step decomposition, which additionally uses a neural network verifier. We show that both traditionally implemented as well as neural network controllers are verified within minutes. The dual focus on formal safety and implementation verification provides a comprehensive framework applicable to similar cyber-physical systems.

A major challenge in autonomous driving is designing control architectures that guarantee safety in all relevant driving scenarios. Given a safe desired reference trajectory for the vehicle, a trajectory following controller has to ensure that the trajectory is followed with a maximally allowed deviation, even in the presence of external disturbances, such as wind gusts or inclined roads. In this paper, a method for computing upper bounds for linear, time invariant single-input-multiple-output systems with state feedback controllers and additive bounded disturbances is proposed. The bounds for the offset between states and the reference are derived analytically based on worst case disturbance sequences. For systems with two states the bounds are strict, while for higher order systems they are conservative. The method is applied to obtain position bounds for lateral trajectory following controllers, and to analyze how different choices of feedback parameters affect safety margins.

We present a new general and language independent approach to the noisy text correction problem developed and implemented in the framework of the CULTURA project. We briefly describe the core candidate generator, REBELS, the complete system concept, its efficient implementation based on functional automata and its immediate applications. The quality of the whole system is empirically established in different experimental settings where language and noise sources are varied.

We describe a novel approach for the extraction of spelling variations from a list of instances. It relates distinctive infixes to distinctive infixes of referenced words. The distinctive infixes are extracted automatically from a (multi)set of instances and a referenced dictionary without any additional expert knowledge. Based on the spelling variations retrieved during a learning(training) phase we develop a correction algorithm which suggests and ranks candidates for a particular noisy word. The main advantage of our approach is that it provides good corrections for the unobserved noisy words while it is almost perfect on words observed during the learning. Our experimental results of the normalisation of a typical reference corpus of Early Modern English letters, [1], significantly improve over previous results of VARD2, [2]. We also achieve better results than those reported in [3] and [4] on the OCR-correction of the TREC-5 Confusion Track corpus,[5].