Considering diverse scenarios in urban traffic, the safety assessment of the decision-making process in automated driving is of great concern for years. And the difficulties of assessing safety lies in the computation of massive spatio-temporal data, the classification of scenarios, and the representation of the uncertainty in the environment with mixed traffic of manned and automated driving. Formal methods are often advocated as the way of increasing confidence in the safety-critical systems via its rigorous mathematical logic. Thus, we propose an assessment scheme which involves: i) the abstract model for decision-making, ii) characterization of composable scenarios, and iii) a corresponding formal verification method to assess safety. The abstract model captures features from the real-time observation and the estimation of the feasible driving alternatives of the surrounding vehicles, as the scenario is regarded as the dynamic evolution of the spatio-temporal data in the static road geometry over time. These features enable the specification and reasoning of the spatial guard conditions and safety properties, and also contribute to the connection and composability of the scenarios. Due to our scenario-based model verification method, we can assess the safety of decisions in scenario transitions by quantitative verification on the probability of the satisfaction of safety property through mapping from our approach to UPPAAL SMC. For illustration, case studies in the fundamental scene structures and the multi-lane roundabout are introduced.

With rapid technological advances in airborne control systems, it has become imperative to ensure the reliability, robustness, and adaptability of airborne software since failure of these software could result in catastrophic loss of property and life. DO-333 is a supplement to the DO-178C standard, which is dedicated to guiding the application of formal methods in the review and analysis of airborne software development processes. However, DO-333 lacks theoretical guidance on how to choose appropriate formal methods and tools to achieve verification objectives at each stage of the verification process, thereby limiting their practical application. This paper is intended to illustrate the formal methods and tools available in the verification process to lay down a general guide for the formal development and verification of airborne software. We utilized the Air Data Computer (ADC) software as the research object and applied different formal methods to verify software lifecycle artifacts. This example explains how to apply formal methods in practical applications and proves the effectiveness of formal methods in the verification of airborne software.

Programmable Logic Controllers (PLCs) are specialized computers extensively utilized in industrial control fields. Since they control industrial equipment, software faults in PLCs can result in significant losses. However, current testing for PLC programs is mainly manual, and there are very few automatic testing tools. Structured Text (ST) is one of the five PLC programming languages stipulated by the IEC 61131-3 standard, suitable for writing complex control logic. This paper proposes an automatic unit test case generation framework for ST programs based on Dynamic Symbolic Execution and PLC states, as well as a supporting algorithm, and implements the PLCAutoTester tool. PLCAutoTester supports the automatic generation of ST program unit test cases that comply with statement coverage, branch coverage, and MC/DC coverage criterion. We evaluated the PLCAutoTester using 20 PLC programs and compared it with S ${}_{YM}$ PLC. The experimental results show that PLCAutoTester can generate unit test cases with high coverage in a short time. And in 11 common programs, PLCAutoTester is able to generate test cases with almost the same statement coverage as S ${}_{YM}$ PLC while reducing the number of test cases by 95%.

Source-free domain adaptation (SFDA) aims to address the challenge of adapting to a target domain without accessing the source domain directly. However, due to the inaccessibility of source domain data, deterministic invariable features cannot be obtained. Current mainstream methods primarily focus on evaluating invariant features in the target domain that closely resemble those in the source domain, subsequently aligning the target domain with the source domain. However, these methods are susceptible to hard samples and influenced by domain bias. In this paper, we propose a Consistent Assistant Domains Transformer for SFDA, abbreviated as CADTrans, which solves the issue by constructing invariable feature representations of domain consistency. Concretely, we develop an assistant domain module for CADTrans to obtain diversified representations from the intermediate aggregated global attentions, which addresses the limitation of existing methods in adequately representing diversity. Based on assistant and target domains, invariable feature representations are obtained by multiple consistent strategies, which can be used to distinguish easy and hard samples. Finally, to align the hard samples to the corresponding easy samples, we construct a conditional multi-kernel max mean discrepancy (CMK-MMD) strategy to distinguish between samples of the same category and those of different categories. Extensive experiments are conducted on various benchmarks such as Office-31, Office-Home, VISDA-C, and DomainNet-126, proving the significant performance improvements achieved by our proposed approaches. Code is available at https://github.com/RoryShao/CADTrans.git.