Static analysis tools have evolved over time to assist in detecting bugs. However, the excessive false warnings can impede developers’ productivity and confidence in the tools. Previous research efforts have explored learning-based approaches to identify bug warnings. Nevertheless, their coarse granularity, focusing on either long-term warnings or function-level alerts, are insensitive to individual bugs. Also, they rely on manually crafted features or solely on source code semantics, which is inadequate for effective learning. In this paper, we propose DeepFWI, a learning-based approach that identifies bug-sensitive warnings at a fine-grained granularity. Specifically, we design a novel LSTM-based model that captures multi-modal semantics of source code and warnings from automated static analysis tools (ASATs) and highlights their correlations with cross-attention. To tackle the data scarcity of training and evaluation, we collected a large-scale dataset of 280,273 warnings. We conducted extensive experiments on the dataset to evaluate DeepFWI. The experimental results demonstrate the effectiveness of our approach, with an F1-score 67.06% for confirming true warnings in a finer-grained manner, significantly outperforming all baselines. Additionally, to validate the practicality of DeepFWI from the perspective of developers, we applied DeepFWI to four popular open-source projects. Our approach filtered out the vast majority of warnings, while still successfully surfacing 25 true bug-related warnings that were confirmed through manual analysis.

Open-source software (OSS) vulnerabilities are increasingly prevalent, emphasizing the importance of security patches. However, in widely used security platforms like NVD, a substantial number of CVE records still lack trace links to patches. Although rank-based approaches have been proposed for security patch tracing, they heavily rely on handcrafted features in a single-step framework, which limits their effectiveness. In this paper, we propose PatchFinder, a two-phase framework with end-to-end correlation learning for better-tracing security patches. In the initial retrieval phase, we employ a hybrid patch retriever to account for both lexical and semantic matching based on the code changes and the description of a CVE, to narrow down the search space by extracting those commits as candidates that are similar to the CVE descriptions. Afterwards, in the re-ranking phase, we design an end-to-end architecture under the supervised fine-tuning paradigm for learning the semantic correlations between CVE descriptions and commits. In this way, we can automatically rank the candidates based on their correlation scores while maintaining low computation overhead. We evaluated our system against 4,789 CVEs from 532 OSS projects. The results are highly promising: PatchFinder achieves a Recall@10 of 80.63% and a Mean Reciprocal Rank (MRR) of 0.7951. Moreover, the Manual Effort@10 required is curtailed to 2.77, marking a 1.94 times improvement over current leading methods. When applying PatchFinder in practice, we initially identified 533 patch commits and submitted them to the official, 482 of which have been confirmed by CVE Numbering Authorities.

Quality assurance (QA) tools are receiving more and more attention and are widely used by developers. Given the wide range of solutions for QA technology, it is still a question of evaluating QA tools. Most existing research is limited in the following ways: (i) They compare tools without considering scanning rules analysis. (ii) They disagree on the effectiveness of tools due to the study methodology and benchmark dataset. (iii) They do not separately analyze the role of the warnings. (iv) There is no large-scale study on the analysis of time performance. To address these problems, in the paper, we systematically select 6 free or open-source tools for a comprehensive study from a list of 148 existing Java QA tools. To carry out a comprehensive study and evaluate tools in multi-level dimensions, we first mapped the scanning rules to the CWE and analyze the coverage and granularity of the scanning rules. Then we conducted an experiment on 5 benchmarks, including 1,425 bugs, to investigate the effectiveness of these tools. Furthermore, we took substantial effort to investigate the effectiveness of warnings by comparing the real labeled bugs with the warnings and investigating their role in bug detection. Finally, we assessed these tools’ time performance on 1,049 projects. The useful findings based on our comprehensive study can help developers improve their tools and provide users with suggestions for selecting QA tools.

Static application security testing (SAST) takes a significant role in the software development life cycle (SDLC). However, it is challenging to comprehensively evaluate the effectiveness of SAST tools to determine which is the better one for detecting vulnerabilities. In this paper, based on well-defined criteria, we first selected seven free or open-source SAST tools from 161 existing tools for further evaluation. Owing to the synthetic and newly-constructed real-world benchmarks, we evaluated and compared these SAST tools from different and comprehensive perspectives such as effectiveness, consistency, and performance. While SAST tools perform well on synthetic benchmarks, our results indicate that only 12.7% of real-world vulnerabilities can be detected by the selected tools. Even combining the detection capability of all tools, most vulnerabilities (70.9%) remain undetected, especially those beyond resource control and insufficiently neutralized input/output vulnerabilities. The fact is that although they have already built the corresponding detecting rules and integrated them into their capabilities, the detection result still did not meet the expectations. All useful findings unveiled in our comprehensive study indeed help to provide guidance on tool development, improvement, evaluation, and selection for developers, researchers, and potential users.

In order to assess the fire risk of the intelligent buildings, a trustworthy classification model was developed, which provides model supporting for the classification assessment of fire risk in intelligent buildings under the urban intelligent firefight construction. The model integrates Bayesian Network (BN) and software trustworthy computing theory and method, designs metric elements and attributes to assess fire risk from four dimensions of fire situation, building, environment and personnel; BN is used to calculate the risk value of fire attributes; Then, the fire risk attribute value is fused into the fire risk trustworthy value by using the trustworthy assessment model; This paper constructs a trustworthy classification model for intelligent building fire risk, and classifies the fire risk into five ranks according to the trustworthy value and attribute value. Taking the Shanghai Jing'an 11.15 fire as an example case, the result shows that the method provided in this paper can perform fire risk assessment and classification.

From the perspective of attribute decomposition, there are a variety of software trustworthiness metric models. However, little attention has been paid to using more rigorous methods and to performing theoretical validation. Axiomatic methods formalise the empirical understanding of software attributes through defining ideal metric properties. They can offer precise terms for the software attributes' quantification. We have utilised them to assess software trustworthiness on the basis of attribute decomposition, presented four properties, constructed a software trustworthiness measure (STMBDA for short). In this paper, we extend the set of properties, introduce two new properties, namely non-negativity and proportionality, and perfect substitutability and expectability. We verify the theoretical rationality of STMBDA by demonstrating that it conforms to the new property set and the empirical validity by evaluating the trustworthiness of 23 spacecraft software. The validation results show that STMBDA is able to effectively assess the spacecraft software trustworthiness and identify weaknesses in the development process.

The Clock Constraint Specification Language (CCSL) is a clock-based formalism for formal specification and analysis of real-time embedded systems. Previous approaches for the schedulability analysis of CCSL specifications are mainly based on model checking or SMT-checking. In this paper we propose a logical approach mainly based on theorem proving. We build a dynamic logic called 'clock-based dynamic logic' (cDL) to capture the CCSL specifications and build a proof calculus to analyze the schedule problem of the specifications. Comparing with previous approaches, our method benefits from the dynamic logic that provides a natural way of capturing the dynamic behaviour of CCSL and a divide-and-conquer way for 'decomposing' a complex formula into simple ones for an SMT-checking procedure. Based on cDL, we outline a method for the schedulability analysis of CCSL. We illustrate our theory through one example.

The Internet of Things (IoT) is announced to swamp the world. In order to understand the emergent behaviour of connected things, effective support for the modelling of connection and failure probabilities, execution and waiting times, as well as resource consumptions of various kinds is needed. At the heart of IoT are flexible and adaptive communication and interaction patterns between things, meant to enable advanced as well as radically new emerging functionalities. Since these interaction patterns are determined by topological characteristics, they can naturally be modelled by channel-based exogenous coordination primitives. In this paper, we tackle the IoT modelling challenge. Our modelling approach is based on a conservative extension of Reo circuits. On a technical level, we work with a model called Priced Probabilistic Timed Constraint Automaton, which combines existing models of probabilistic and timed aspects, and is equipped with pricing information. The latter enables us to reason about resource consumption, especially important in light of severely limited power, memory and computation budgets in things. The approach is set up in such a way that the original constituent models can be retrieved without changes in syntax and semantics. A small but illustrative IoT case is modelled and evaluated, demonstrating the principal benefits of the proposed approach.

The behavioural distance is a more robust way of formalising behavioural similarity between states than bisimulations. The smaller the distance, the more alike the states are. It is helpful for quantitative verifications of concurrent systems. The main contribution of this paper is an effective procedure for computing behavioural distance introduced by Cao et al. (IEEE Transactions on Fuzzy Systems, 21 (2013) 735-747). The time complexity of the algorithm is O(n5m3lg n), where n is the number of states and m is the number of transitions in the underlying transition systems. The key step in this algorithm is to compute the distance between two distributions, which is defined as the value of a mathematical programming problem (MP). In this process, some interesting properties about solutions of a fuzzy system, which is a constraint of the MP, are discussed.

Pipe protocol, proposed by Zhao [1] in early 2013, is one application layer protocol and one way to establish the Internet of Things, under which can different kinds of hardware platforms communicate with each other faster and more safely. As an upper layer protocol, Pipe protocol doesn't define details, but during the implementation, probabilistic and nondeterministic behaviors, such as data loss and external choice, are possible to happen. In this paper, we use probabilistic model checker, PRISM, to construct the probabilistic Pipe protocol as Probabilistic Timed Automata (PTAs), then verify some useful time-bounded properties, written in Probabilistic Computation Tree Logic (PCTL), like, “Maximum probability that the pipe is shut down after Source node sends all 5 data packets within 50 μs”. The results show that the data loss probabilities, number of data and deadline should be restricted suitably if we require the maximum probability of the goal reaches some value. Our model is proved to be meaningful and we can give helpful suggestions to improve the implementation of Pipe protocol.

This paper introduces a domain Spatio-Temporal Consistency (STeC) language for the application domain of space-air-ground integrated networks. The STeC language is taken as the foundation of modeling our systems, bacause it works well on specifying real-time systems concerning not only the time characteristic but also the location characteristic and the consistency between them. In this paper, a domain-STeC language is devised and applied to model satellite observation processes. We use two tools to check and verify this STeC model, the syntax and spatio-temporal consistency were checked in STeC tool, and after being transformed into timed automata model, some further verification can be finished in UPPAAL tool. It shows that the instantiated STeC approach is suitable for modeling and verifying space-air-ground integrated networks on the requirement level. This work helps to ensure the spatial-temporal consistency in that application domain, and increases the reliability and dependability of our system.

Intelligent Transportation Systems (ITS) are a class of quickly evolving modern safety-critical embedded systems. Dealing with their growing complexity demands a high-level formal modeling language along with adequate verification techniques. STeC has recently been introduced as a process algebra that deals natively with both spatial and temporal properties. Even though STeC has the right expressive power, it does not provide a direct tooled support for verification. We propose to encode STeC specifications as Timed Automata to provide such a support and we illustrate our transformation strategy on a simple example.

To model and analyze systems with multi-valued information, in this paper, we present an extension of Kripke structures in the framework of complete residuted lattices, which we will refer to as lattice-valued Kripke structures (LKSs). We then show how the traditional trace containment and equivalence relations, can be lifted to the lattice-valued setting, and we introduce two families of lattice-valued versions of the relations. Further, we explore some interesting properties of these relations. Finally, we provide logical characterizations of our relations by a natural extension of linear temporal logic.

In order to describe the requirement of spatial and temporal consistency of cyber-physical systems, a specification language called as STeC was proposed by Chen in [1]. In this paper, we focus on the theory of semantics of STeC. After simply restating the syntax and operational semantics, we mainly establish the denotational semantics of STeC. To investigate the reasonability of the denotational semantics, an abstract theorem is given to show the soundness and completeness of the denotational semantics. Finally, a simple case about China Gaotie (which means High-speed train) is given to show how to compute the operational and denotational semantics.

In this paper, we define lattice-valued labeled transition systems (LLTS) as a general framework for allowing imprecise or incomplete specifications to be expressed. We introduce a lattice-valued bisimulation between LLTSs that measures the degree of closeness of two systems as elements of residuated lattice, in contrast to the traditional boolean yes/no to bisimulation. Also, we show that our bisimulation is compositional for a synchronous composition operator. Moreover, we also consider lattice-valued extension of Kripke structures, define a lattice-valued bisimulation between lattice-valued Kripke structures (LKSs), and establish the correspondence between lattice-valued bisimulation in LLTS and lattice-valued bisimulation in LKS.

Many researchers suggested extending bisimilarity to quantitative versions to avoid the rigidity of classical bisimilarity. To explore the relation between different notions of approximate bisimilarity mentioned in literature, in this paper, we present a quantitative extension of doubly labeled transition systems, MDLTS, where its states and actions form metric spaces. We then introduce two notions of approximate bisimilarity, (η, λ)-bisimilarity and (η, λ, α)-bisimilarity, and discuss their basic property. We also consider the special kind of (η, λ)-bisimilarity, λ-bisimilarity to characterize the branching distance with arbitrary discount α of metric labeled transition system. Finally, we discuss the translation between metric transition system and MDLTS which preserves the approximate bisimilarity.

In this paper, we focus on the infinite evolution of the parameterized bisimulation in order to discuss the dynamic characterization of programs. We propose parameterized limit bisimulation and parameterized bisimulation limit which are useful for understanding and analyzing of infinite evolution of concurrent programs. Some special parameterized limit bisimulations are introduced and some topological properties are proved.