Testing-based formal verification (TBFV) is proposed to reduce test cost and guarantee software reliability by ensuring the correctness of all traversed program paths. An ideal target is to generate adequate test cases to traverse all of its execution paths. However, it is a rather ambitious criterion that can hardly be satisfied due to the potentially great amount of test cases required. To address this problem, we propose a new criterion called Condition Sequence Coverage (CSC) to maintain a good balance between program correctness and the number of test cases. In this paper, we refine the TBFV method and introduce the theoretical foundations of CSC. We also integrate CSC with functional scenario form (FSF) to automatically generate test cases for the TBFV method. In addition, we develop the tool support for Java and validate its effectiveness and accuracy through experimental comparisons.

Adversarial examples have become a critical focus in ensuring the security and robustness of deep learning (DL) systems. In this paper, we introduce an innovative approach for generating adversarial examples, designed to identify and diagnose common errors in DL models. Specifically, our method targets two key issues: Oscillating Loss (OL) and Slow Convergence (SC), providing valuable insight into model performance and fault detection. Using a reinforcement learning framework, we generate test data that effectively distinguishes between models with and without these errors. We consider the MNIST and CIFAR-10 datasets and test our approach on neural networks with various architectures, demonstrating significant improvements in error detection across different types of models. These results highlight the substantial effectiveness of our proposed method in improving the reliability of DL models. Furthermore, we demonstrate the scalability of our approach, showing that it can be used to diagnose various common errors in DL models with minimal modifications.

Neural networks are extensively employed in safety-critical systems. However, these critical systems incorporating neural networks continue to pose risks due to the presence of adversarial examples. Although the security of neural networks can be enhanced by verification, verifying neural networks is an NP-hard problem, making the application of verification algorithms to large-scale neural networks a challenging task. For this reason, we propose NNTBFV, a framework that utilizes the principles of Testing-Based Formal Verification (TBFV) to simplify neural networks and verify the simplified networks. Unlike conventional neural network pruning techniques, this approach is based on specifications, with the goal of deriving approximate execution paths under given preconditions. To mitigate the potential issue of unverifiable conditions due to overly broad preconditions, we also propose a precondition partition method. Empirical evidence shows that as the range of preconditions narrows, the size of the execution paths also reduces accordingly. The execution path generated by NNTBFV is still a neural network, so it can be verified by verification tools. In response to the results from the verification tool, we provide a theoretical method for analysis. We evaluate the effectiveness of NNTBFV on the ACAS Xu model project, choosing Verification-based and Random-based neural network simplification algorithms as the baselines for NNTBFV. Experiment results show that NNTBFV can effectively approximate the baseline in terms of simplification capability, and it surpasses the efficiency of the random-based method.

Human–Machine Pair Programming (HMPP) is a promising technique in the software development process, which means that software construction can be done in the manner that humans are responsible for developing the program while computer is responsible for monitoring the program in real-time and reporting errors. The Java runtime exceptions in the current version of the software under construction can only be effectively detected by means of its execution. Traditional software testing techniques are suitable for testing completed programs but face a challenge in building a suitable testing environment for testing the partial programs produced during HMPP. In this paper, we put forward a novel technique, called Program Segment Testing (PST) for automatically identifying errors caused by runtime exceptions to support HMPP. We first introduce the relevant involved in this technique to detect index out of bounds exceptions, a representative of runtime exceptions. Then we discuss the methodology of this technique in detail and illustrate its workflow with a simple case study. Finally, we carry out an experiment to evaluate this technique and compare it with three existing fault detection techniques using several programs to demonstrate its effectiveness.

Human-Machine Pair Inspection (HMPI) is a novel code inspection technology proposed in our previous work, which is the style that machine will intelligently guide the programmer to carry out inspections of the program code during programming. For large-scale software projects, the efficiency of HMPI needs to be improved due to the inaccurate measurement of the code structure and the excessive inspection scope. In this paper, to alleviate the above deficiencies, we propose the Risk Number, a code evaluation metric generated based on historical error data. The Risk Number is calculated by a statistical tool called regression analysis, which more accurately indicates the relationship between the nested structure of the code and the likelihood of containing bugs than Cognitive Complexity. Additionally, HMPI is supported by utilizing Risk Number to point out high-risk code and program slicing techniques to extract statements that have dependencies on the code to generate checklists, thereby reducing the scope of inspection. We describe a case study to evaluate the performance of this method by comparing its inspection time and number of detected errors with our previous work. The result shows that the method is likely to guide the programmer to inspect the faulty code earlier and be more efficient in detecting defects than HMPI based on Cognitive Complexity.

Testing a program based on its specification is necessary to ensure that the program meets its desired functionality. Formal methods, based on some mathematical theories, are often used to enhance the quality of systems but suffer from difficulties in application. The Testing-Based Formal Verification (TBFV) is proposed as an alternative to ensure the correctness of all traversed program paths, but is limited and impractical due to the lack of the capability of dealing with operations (e.g., methods defined in classes) provided in software packages. In this paper, we provide an axiomatic approach to dealing with this problem so as to enhance the capability of the TBFV. In particular, we focus on the Vector, ArrayList, and LinkedList classes in Java. We present both an example to demonstrate how our approach works properly and two small experiments conducted to evaluate the performance of our approach by comparing it with the specification-based testing (SBT). The result shows that our approach is more than 30% superior to the SBT in bug detection.

Formal specifications can provide a solid foundation for software development and support for techniques of software quality assurance, such as specification-based inspection and testing. To ensure that these techniques can be applied effectively in practice, efficiently and accurately understanding specifications becomes extremely important. While this may be relatively easy for well-trained developers in formal methods, it can be rather difficult for computer since computer does not easily understand specifications. This difficulty poses a challenge for realizing automatic specification-based verification techniques that are in high demand for reducing development cost and improving software reliability. In this paper, we address this problem by discussing how the formal specification can be transformed into a knowledge graph to provide comprehensible, well-organized details of the specification for developers and computers. The transformation is done by extracting and storing information about attributes of each component and by establishing relationships between components in a formal specification. We elaborate on a top-down approach of constructing a knowledge graph from a specification, including creating an ontology, designing the Entity–Relationship (ER) diagram of the relational database based on the created ontology, extracting and storing attribute and relationship information in the relational database, mapping ontology to its instances and relational data to RDF triples, and displaying knowledge graph. Further, we present a case study to show how our approach works on the formal specification of an ATM system. Finally, we describe three experiments to evaluate its performance in improving specification readability, effectively guiding inspectors to establish traceability links between specifications and programs, and detecting defects through program inspection, respectively.

Software defect prediction is aimed at helping developers to quickly locate defective components in the code repository and thus better allocate resources. However, most of the current traditional defect prediction methods mainly depend on the design of static metrics, but these methods ignore the semantic and structural information of the code. As a result, researchers have turned to building models by extracting semantic features from code through abstract syntax trees. In this article, we introducegated homogeneous fusion networkfor defect prediction namely GHFNet, jointing high-level semantic feature extraction and weighted static feature extraction. Through the mechanism of homogeneous gating fusion, weights are adaptively assigned to the two types of features based on the correlation of these features to form fused features for defect prediction in the code. Experimental results show that the proposed approach is a significant improvement. Specifically, for the reference method we present GHFNet improved from 9.4 to 15.2 percentage points in effort-unaware scenarios (F-measure) and from 3.7 to 8 percentage points in effort-aware scenarios (Popt) for defect prediction.

Software defect prediction plays a significant role in the software development cycle but suffers from many difficulties. In this paper we propose a novel deep learning model (including algorithms) called Extractor, Parser, and Reviewer (EPR) for defect prediction in software. Two different networks, recurrent neural networks (RNNs) and one-dimensional convolutional networks(ODCNs), are employed by the EPR for different purposes. RNN is utilized to extract contextual features to represent semantic dependencies between code tokens and ODCN acts as a parser to establish dependencies between semantic features. Meanwhile, the attention mechanism of the two networks is used as a reviewer to assign different weights from location information to the importance of the features, respectively. Our proposed model is validated by the PROMISE repository, and the results show that the proposed model in this paper significantly outperforms several existing algorithms.

Linking the components in a formal specification to those in the corresponding program is a prerequisite for formal specification-based program fault detection. Existing traceability link techniques for reducing manpower and time cost suffer from the limitation in effectiveness due to over dependency of textual similarity. Unlike the existing work, this paper presents an automatic method for constructing traceability links between SOFL formal specifications and Java codes, taking semantical, structural, functional, and relational similarities measures into account. It operates at multiple levels of a formal specification, such as data flows, processes, and modules, to establish finegrained link relationships between artifacts. Further, a comparative evaluation of the proposed method, using two selected modules of the SOFL formal specification of a critical ATM system and its Java implementation with 951 code of lines, demonstrates an improvement in precision and more generality than existing latent semantic indexing that is an information retrieval-based method.

As a quantum counterpart of labeled transition system (LTS), quantum labeled transition system (QLTS) is a powerful formalism for modeling quantum programs or protocols, and gives a categorical understanding for quantum computation. With the help of quantum branching monad, QLTS provides a framework extending some ideas in non-deterministic or probabilistic systems to quantum systems. On the other hand, quantum finite automata (QFA) emerged as a very elegant and simple model for resolving some quantum computational problems. In this paper, we propose the notion of reactive quantum system (RQS), a variant of QLTS capturing reactive system behavior, and develop a coalgebraic semantics for QLTS, RQS and QFA by an endofunctor on the category of convex sets, which has a final coalgebra. Such a coalgebraic semantics provides a unifying abstract interpretation for QLTS, RQS and QFA. The notions of bisimulation and simulation can be employed to compare the behavior of different types of quantum systems and judge whether a coalgebra can be behaviorally simulated by another.