Automated driving systems (ADS) are constrained by the limits of onboard perception, especially when visual obstructions create hazards. Using external data, such as V2X hazard messages, can mitigate these shortcomings but may introduce additional hazards due to their unreliability. We propose an Early Hazard Processing System (EHPS) that informs an extended ADS about external hazards, enabling it to perform proactive risk mitigation. Extended ADS has a cautious state that proactively reduces speed and applies comfort-bounded deceleration when EHPS reports potential hazards. All other safety-critical actions depend on internal sensor confirmation and remain under the control of ADS fallback mechanisms. Our proposed solution is formalised with a three-state model that is shown to be as safe as baseline ADS, supported by safety argumentation. Finally, our simulation-based evaluation using the Automated Lane Keeping System shows how early awareness provides more reaction time and more comfortable braking, even when external information is unreliable. Our results show that even unreliable external hazard data improves ADS safety and comfort without compromising baseline safety guarantees.

Autonomous driving functions (ADFs) are becoming more relevant and complex. Still, their safe and correct operation must be guaranteed. Scenario-based testing, i.e. confronting the ADF under test with other traffic in specified scenarios is an established approach for the validation and verification of ADFs, but tests currently often only consider simple technical requirements. Safe and correct operation is not only the absence of collisions but involves complex spatio-temporal requirements on the externally observable, functional driving behaviour in traffic. In this work, we consider Traffic Sequence Charts (TSCs) as a visual formalism for the specification of complex, functional ADF requirements. We define a monitoring problem for TSCs and finite, sampled observations of ADF behaviour and discuss how monitor verdicts contribute to requirements testing. We show that such monitors can effectively be constructed for realistic requirements and that they can contribute to efficient testing by assessing ADF behaviour at runtime.

The European GAIA-X project aims to create an innovative open, transparent and secure data infrastructure for different domains like energy, agriculture, and mobility. Data providers and consumers from one domain are supposed to form a data ecosystem on this infrastructure. Developing a new GAIA-X ecosystem for a particular domain is challenging because the participants of the ecosystems develop new business models and specifications of novel services while refining the requirements on the GAIA-X infrastructure, which is currently under construction. There is a need for approaches that help the consortium of participants in this innovation exploration task, i.e. to handle the complexity and provide communication means on a right level of abstraction. The Innovation Modeling Grid (IMoG) is an innovation modeling methodology with well-defined procedures that can help understand the GAIA-X problem space and present the model concisely. We applied IMoG as an innovation modeling approach on a GAIA-X ecosystem focused on mobility. In this paper, we present our experiences gained during this study. We found that using IMoG led to a better understanding of the roles, services, and interfaces in a specific GAIA-X ecosystem.

Software systems continue to pervade day-to-day life and so it becomes increasingly important to ensure the dependability, safety, and security of software. One approach to this end can be summarised under the broad term of formal methods, i.e., the formal analysis of requirements, software models, or programs. Formal methods in this sense are today used in many branches of the software industry, such as the huge internet companies, aerospace, automotive, etc. and even made their way into small to medium sized enterprises. In this article, we argue the opinion that today's students (and tomorrow's engineers) need to be provided with a basic understanding of formal methods in the broad sense (what is it, how does it feel to use it, what are advantages and limitations) already in undergraduate introductions to software engineering. We propose a generic course design that complements (otherwise completely ordinary) undergraduate introductions to software engineering with formal semantics and analyses of (visual) software description languages. We report on five years of teaching an implementation of the course design that indicate the feasibility of teaching without sacrificing classical software engineering topics and without over-straining students wrt. level or workload.

Detecting issues in real-time requirements is usually a trade-off between flexibility and cost: the effort expended depends on how expensive it is to fix a defect introduced by faulty, ambiguous or incomplete requirements. The most rigorous techniques for real-time requirement analysis depend on the formalisation of these requirements. Completely formalised real-time requirements allow the detection of issues that are hard to find through other means, like real-time inconsistency (i.e., "do the requirements lead to deadlocks and starvation of the system?") or vacuity (i.e., "are some requirements trivially satisfied"). Current analysis techniques for real-time requirements suffer from scalability issues - larger sets of such requirements are usually intractable. We present a new technique to analyse formalised real-time requirements for various properties. Our technique leverages recent advances in software model checking and automatic theorem proving by converting the analysis problem for real-time requirements to a program analysis task. We also report preliminary results from an ongoing, large scale application of our technique in the automotive domain at Bosch.

Quasi-equal clocks reduction for networks of timed automata yields significant savings in verification costs of properties of timed automata by replacing clocks in equivalence classes by representative clocks. In this work we present the theoretical analysis that quantifies and justifies those savings. We propose new space and time bounds that characterise a less expensive model checking effort in transformed networks wrt. The effort in original networks with quasi-equal clocks. Additionally, we carry out improvements to our transformation algorithm in order to maximize savings wrt. Space and time, and we eliminate all remaining semantic assumptions on networks introduced to soundly apply the reduction of clocks.

Abstract The design of distributed, safety-critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions that stem from international standards. We present a case study that shows that despite those challenges, the automated formal verification of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless fire alarm system, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification tests for a relevant regulation standard will be passed. In general we observe that if system tests are specified by generalized test procedures, then verifying that a system will pass any test following those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.

The concept of hybrid automata provides a powerful framework to model and analyze real-world systems. Due to the structural complexity of hybrid systems it is important to ensure the scalability of analysis algorithms. We approach this problem by providing an effective generalisation of the recently introduced notion of quasi-equal clocks to hybrid systems. For this purpose, we introduce the concept of quasi-dependent variables. Our contribution is two-fold: we demonstrate how such variables can be automatically detected, and we present a transformation leading to an abstraction with a smaller state space which, however, still retains the same properties as the original system. We demonstrate the practical applicability of our methods on a range of industrial benchmarks.

We propose a design and verification methodology supporting the early phases of system design for cooperative driver assistance systems, focusing on the realisability of new automotive functions. Specifically, we focus on applications where drivers are supported in complex driving tasks by safe strategies involving the coordinated movements of multiple vehicles to complete the driving task successfully. We propose a divide and conquer approach for formally verifying timed probabilistic requirements on successful completion of the driving task and collision freedom based on formal specifications of a set of given manoeuvring and communication capabilities of the car. In particular, this allows an assessment of whether they are sufficient to implement strategies for successful completion of the driving task.

Natural language safety requirements in industrial standards pose risks for ambiguities which need to be resolved by the system manufacturer in concertation with the certificate authority. This is especially challenging for small and medium-sized enterprises (SME). In this paper we report on our experiences with applying traditional requirements engineering techniques, formal methods, and visual narratives in an exploratory case-study in an SME.