arXiv subjects

Dejan Ničković

Publications and source records attributed to Dejan Ničković.

12 recordsLinked to original sources

arXiv2026

Automatic Testing of Interacting Autonomous Vehicles

Autonomous vehicles (AVs) must be thoroughly tested to meet high safety standards and avoid endangering both AV passengers and road users. Scenario-based testing implements driving scenarios in virtual simulation environments as a cost-effective alternative to field testing. Common scenario-based testing approaches set the environment and the surrounding traffic and test a single AV. Recent studies show that the approaches that test single AVs miss critical behaviors that emerge from interactions among multiple AVs. Effective approaches to test scenarios that emerge from n-way interactions must address the combinatorial explosion that the presence of multiple AVs further exacerbates. In this paper, we propose EVITA, an approach that leverages multi-objective optimization to generate scenarios that trigger multiple and diverse AVs interactions, while minimizing the complexity of the generated scenarios, to effectively test multiple interacting AVs and reveal safety-critical scenarios that current approaches overlook. The experimental results that we discuss in this paper confirm that EVITA triggers a higher variety of AVs interactions than state-of-the-art approaches, thus improving the likelihood to reveal safety-critical behaviors.

cs.SE↗

arXiv2026

Declarative Scenario-based Testing with RoadLogic

Scenario-based testing is a key method for cost-effective and safe validation of autonomous vehicles (AVs). Existing approaches rely on imperative scenario definitions, requiring developers to manually enumerate numerous variants to achieve coverage. Declarative languages, such as ASAM OpenSCENARIO DSL (OS2), raise the abstraction level but lack systematic methods for instantiating concrete and specification-compliant scenarios. To our knowledge, currently, no open-source solution provides this capability. We present RoadLogic that bridges declarative OS2 specifications and executable simulations. It uses Answer Set Programming to generate abstract plans satisfying scenario constraints, motion planning to refine the plans into feasible trajectories, and specification-based monitoring to verify correctness. We evaluate RoadLogic on instantiating representative OS2 scenarios executed in the CommonRoad framework. Results show that RoadLogic consistently produces realistic, specification-satisfying simulations within minutes and captures diverse behavioral variants through parameter sampling, thus opening the door to systematic scenario-based testing for autonomous driving systems.

cs.SE↗

arXiv2025

TD-Interpreter: Enhancing the Understanding of Timing Diagrams with Visual-Language Learning

We introduce TD-Interpreter, a specialized ML tool that assists engineers in understanding complex timing diagrams (TDs), originating from a third party, during their design and verification process. TD-Interpreter is a visual question-answer environment which allows engineers to input a set of TDs and ask design and verification queries regarding these TDs. We implemented TD-Interpreter with multimodal learning by fine-tuning LLaVA, a lightweight 7B Multimodal Large Language Model (MLLM). To address limited training data availability, we developed a synthetic data generation workflow that aligns visual information with its textual interpretation. Our experimental evaluation demonstrates the usefulness of TD-Interpreter which outperformed untuned GPT-4o by a large margin on the evaluated benchmarks.

cs.LG↗

arXiv2024

Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy

In distributed systems with processes that do not share a global clock, \emph{partial synchrony} is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an \emph{approximate} distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.

cs.LO↗

arXiv2023

A Systematic Approach to Automotive Security

We propose a holistic methodology for designing automotivesystems that consider security a central concern at every design stage.During the concept design, we model the system architecture and definethe security attributes of its components. We perform threat analysis onthe system model to identify structural security issues. From that analysis,we derive attack trees that define recipes describing steps to successfullyattack the system's assets and propose threat prevention measures.The attack tree allows us to derive a verification and validation (V&V)plan, which prioritizes the testing effort. In particular, we advocate usinglearning for testing approaches for the black-box components. It consistsof inferring a finite state model of the black-box component from its executiontraces. This model can then be used to generate new relevanttests, model check it against requirements, and compare two differentimplementations of the same protocol. We illustrate the methodologywith an automotive infotainment system example. Using the advocated approach, we could also document unexpected and potentially criticalbehavior in our example systems.

cs.CR↗

arXiv2023

Specification-Guided Critical Scenario Identification for Automated Driving

To test automated driving systems, we present a case study for finding critical scenarios in driving environments guided by formal specifications. To that aim, we devise a framework for critical scenario identification, which we base on open-source libraries that combine scenario specification, testing, formal methods, and optimization.

math.OC↗

arXiv2022

Hierarchical Potential-based Reward Shaping from Task Specifications

The automatic synthesis of policies for robotic-control tasks through reinforcement learning relies on a reward signal that simultaneously captures many possibly conflicting requirements. In this paper, we in\-tro\-duce a novel, hierarchical, potential-based reward-shaping approach (HPRS) for defining effective, multivariate rewards for a large family of such control tasks. We formalize a task as a partially-ordered set of safety, target, and comfort requirements, and define an automated methodology to enforce a natural order among requirements and shape the associated reward. Building upon potential-based reward shaping, we show that HPRS preserves policy optimality. Our experimental evaluation demonstrates HPRS's superior ability in capturing the intended behavior, resulting in task-satisfying policies with improved comfort, and converging to optimal behavior faster than other state-of-the-art approaches. We demonstrate the practical usability of HPRS on several robotics applications and the smooth sim2real transition on two autonomous-driving scenarios for F1TENTH race cars.

cs.LG↗

arXiv2022

DeepSTL -- From English Requirements to Signal Temporal Logic

Formal methods provide very powerful tools and techniques for the design and analysis of complex systems. Their practical application remains however limited, due to the widely accepted belief that formal methods require extensive expertise and a steep learning curve. Writing correct formal specifications in form of logical formulas is still considered to be a difficult and error prone task. In this paper we propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems, used both by academia and advanced research labs in industry. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. We propose a two-step workflow to address this challenge. We first design a grammar-based generation technique of synthetic data, where each output is a random STL formula and its associated set of possible English translations. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL. The experimental results show high translation quality for patterns of English requirements that have been well trained, making this workflow promising to be extended for processing more complex translation tasks.

cs.CL↗

arXiv2022

Model-Free Reinforcement Learning for Symbolic Automata-encoded Objectives

Reinforcement learning (RL) is a popular approach for robotic path planning in uncertain environments. However, the control policies trained for an RL agent crucially depend on user-defined, state-based reward functions. Poorly designed rewards can lead to policies that do get maximal rewards but fail to satisfy desired task objectives or are unsafe. There are several examples of the use of formal languages such as temporal logics and automata to specify high-level task specifications for robots (in lieu of Markovian rewards). Recent efforts have focused on inferring state-based rewards from formal specifications; here, the goal is to provide (probabilistic) guarantees that the policy learned using RL (with the inferred rewards) satisfies the high-level formal specification. A key drawback of several of these techniques is that the rewards that they infer are sparse: the agent receives positive rewards only upon completion of the task and no rewards otherwise. This naturally leads to poor convergence properties and high variance during RL. In this work, we propose using formal specifications in the form of symbolic automata: these serve as a generalization of both bounded-time temporal logic-based specifications as well as automata. Furthermore, our use of symbolic automata allows us to define non-sparse potential-based rewards which empirically shape the reward surface, leading to better convergence during RL. We also show that our potential-based rewarding strategy still allows us to obtain the policy that maximizes the satisfaction of the given specification.

cs.AI↗

arXiv2021

Challenges of engineering safe and secure highly automated vehicles

After more than a decade of intense focus on automated vehicles, we are still facing huge challenges for the vision of fully autonomous driving to become a reality. The same "disillusionment" is true in many other domains, in which autonomous Cyber-Physical Systems (CPS) could considerably help to overcome societal challenges and be highly beneficial to society and individuals. Taking the automotive domain, i.e. highly automated vehicles (HAV), as an example, this paper sets out to summarize the major challenges that are still to overcome for achieving safe, secure, reliable and trustworthy highly automated resp. autonomous CPS. We constrain ourselves to technical challenges, acknowledging the importance of (legal) regulations, certification, standardization, ethics, and societal acceptance, to name but a few, without delving deeper into them as this is beyond the scope of this paper. Four challenges have been identified as being the main obstacles to realizing HAV: Realization of continuous, post-deployment systems improvement, handling of uncertainties and incomplete information, verification of HAV with machine learning components, and prediction. Each of these challenges is described in detail, including sub-challenges and, where appropriate, possible approaches to overcome them. By working together in a common effort between industry and academy and focusing on these challenges, the authors hope to contribute to overcome the "disillusionment" for realizing HAV.

cs.AI↗

arXiv2021

Adaptive Testing for Specification Coverage

Ensuring correctness of cyber-physical systems (CPS) is an extremely challenging task that is in practice often addressed with simulation based testing. Formal specification languages, such as Signal Temporal Logic (STL), are used to mathematically express CPS requirements and thus render the simulation activity more systematic and principled. We propose a novel method for adaptive generation of tests with specification coverage for STL. To achieve this goal, we devise cooperative reachability games that we combine with numerical optimization to create tests that explore the system in a way that exercise various parts of the specification. To the best of our knowledge our approach is the first adaptive testing approach that can be applied directly to MATLAB\texttrademark\; Simulink/Stateflow models. We implemented our approach in a prototype tool and evaluated it on several illustrating examples and a case study from the avionics domain, demonstrating the effectiveness of adaptive testing to (1) incrementally build a test case that reaches a test objective, (2) generate a test suite that increases the specification coverage, and (3) infer what part of the specification is actually implemented.

cs.SE↗

arXiv2019

Automatic Failure Explanation in CPS Models

Debugging Cyber-Physical System (CPS) models can be extremely complex. Indeed, only the detection of a failure is insuffcient to know how to correct a faulty model. Faults can propagate in time and in space producing observable misbehaviours in locations completely different from the location of the fault. Understanding the reason of an observed failure is typically a challenging and laborious task left to the experience and domain knowledge of the designer. \n In this paper, we propose CPSDebug, a novel approach that by combining testing, specification mining, and failure analysis, can automatically explain failures in Simulink/Stateflow models. We evaluate CPSDebug on two case studies, involving two use scenarios and several classes of faults, demonstrating the potential value of our approach.

cs.SE↗