Engineering of Complex Computer Systems

To ensure the high availability of modern online systems, effective maintenance is of critical importance. Today’s software maintenance techniques for online systems heavily rely on metrics, which are time series data that can describe the real-time state of a system from various perspectives. Typically, software engineers generate dashboards with metrics to aid software maintenance. Though several attempts have been devoted to metric analysis for automatic software maintenance, the primary step, i.e., dashboard generation, remains manual to a large extent. In this paper, we develop a metric recommendation service, which can automate the dashboard generation practice and greatly ease the burden in maintaining an online system. Specifically, we analyze the needs of two essential steps of online system maintenance, i.e., anomaly detection and fault diagnosis, and design metric recommendation mechanisms for them respectively. Graph learning techniques are employed in the automation of metric recommendation. Our experiments demonstrate that the proposed approach can achieve an F1-score of 0.912 in selecting metrics for anomaly detection, and an accuracy of 0.859 in retrieving metrics for faults diagnosis, which significantly outperforms the compared baselines.

The growing cyber threat landscape necessitates robust defenses, with Network Intrusion Detection Systems (NIDS) at the forefront. Leveraging Deep Neural Networks (DNN) has significantly improved detection accuracy in NIDS. Nonetheless, the inherent data imbalance between malicious and normal network traffic impairs the efficacy of DNN-based methods. Traditional approaches employ Generative Adversarial Networks (GANs) to mitigate this by generating minority class samples. However, these methods often struggle with the scarcity of specific data types during training, leading to low-quality synthetic samples and sub-optimal detection performance.

Addressing this, we introduce the Synchronous Classifier Wasserstein Generative Adversarial Network (SC-WGAN). This novel model extends the WGAN framework by integrating a classifier that processes all traffic data types. This classifier collaborates with the discriminator during the training process, guiding the generator to produce higher-quality synthetic samples. We evaluate SC-WGAN’s performance on three well-known open-source benchmark datasets. Additionally, we compare it against contemporary GAN-based solutions tackling data imbalance. Our findings reveal that SC-WGAN, surpasses existing methods in generating more representative samples and enhancing NIDS detection accuracy.

The problem of configuring the variability models is pervasive in plenty of domains. Renault, a leading automobile manufacturer, has developed an internal product configuration system to model its vehicle diversity. This system is based on the well-known knowledge compilation approach and is associated with a set of parameters. Different input parameters have a strong influence on the system’s performance. The parameters actually used are determined manually. Our work aims to study and determine these parameters automatically. This paper studies Renault’s variability models and product configuration system and presents a parameter prediction model for this system. The results show the predicted parameters’ competitiveness compared with the parameters by default.

Adversarial examples reveal the vulnerability of neural networks, thereby increasing the demand for formal verification of their robustness. Verification methods employing branch and bound technique have shown excellent performance for this task and are widely adopted to provide robustness assurance. A key component in branch and bound is the branching strategy, which determines how to split the feasible region. A good branching strategy can reduce the number of branches that need to be explored, and thus improve the verification efficiency. In this paper, we present a novel branching strategy. For each sub-problem in the branch and bound process, we use its optimal solution to compute a score for each branching choice. This score approximates the potential improvement brought by branching at that choice, and a higher score indicates a better branching decision. Our branching strategy also includes out-of-bound compensation and score truncation. These techniques can help better assess the quality of each branching choice. In addition, we demonstrate that some sub-problems generated by certain branching choice can be directly resolved, which reduces the number of calls to the bounding algorithm. We implement our branching strategy as OptGBS and conduct experiments on widely used open source benchmarks to evaluate its performance. Experimental results show that our branching strategy achieves a roughly 25% time cost reduction compared to the state-of-the-art branching strategies, and verification methods using our branching strategy can achieve higher verified accuracy.

Deep Neural Networks (DNNs) have found successful applications in various non-safety-critical domains. However, given the inherent lack of interpretability in DNNs, ensuring their prediction accuracy through robustness verification becomes imperative before deploying them in safety-critical applications. Neural Network Verification (NNV) approaches can broadly be categorized into exact and approximate solutions. Exact solutions are complete but time-consuming, making them unsuitable for large network architectures. In contrast, approximate solutions, aided by abstraction techniques, can handle larger networks, although they may be incomplete. This paper introduces AccMILP, an approach that leverages abstraction to transform NNV problems into Mixed Integer Linear Programming (MILP) problems. AccMILP considers the impact of individual neurons on target labels in DNNs and combines various relaxation methods to reduce the size of NNV models while ensuring verification accuracy. The experimental results indicate that AccMILP can reduce the size of the verification model by approximately 30% and decrease the solution time by at least 80% while maintaining performance equal to or greater than 60% of MIPVerify. In other words, AccMILP is well-suited for the verification of large-scale DNNs.

In recent years, the emerging open source RISC-V architecture has gradually attracted wide attention. In order to support the compilation of multiple Linux operating system distribution images and packages, developers need to build and adapt the packages. Due to the complexity of software packages and the diversity of developer experience levels, the success of software package construction is uncertain. Existing research lacks automatic classification methods for the reasons of RISC-V architecture software package construction failures. Therefore, an automatic classification model Word2Vec-BERT-bmu is proposed to effectively and automatically locate software package construction failures. Firstly, two popular Linux distribution building platforms, OpenSuse and OpenEuler, were selected as the sources of build failure log data, and 10 types of build failures were manually analyzed and summarized. Secondly, the Word2Vec-BERT-bmu model is proposed to construct the failure classification using an automated software package with multi-feature concatenation. Experimental results show that the Macro F1 value is improved by 2–4% compared with other models. In addition, for real-world software packages, the effectiveness and accuracy of our model we proposed are further verified by manual repair of software packages.

In practices, test cases are often designed by test engineers based on the functionalities of the System under Test (SUT) in parallel and independently. This can lead to a lack of a comprehensive overview of the test architecture, hampering the reuse of test functions when implementing new test cases. To address this challenge, we propose ATAG, an automated test architecture generation approach, which employs an optimization algorithm to retrieve highly cohesive and loosely coupled test functions based on control flows and data flows of test cases. We also equip ATAG with a newly proposed BERT-based model, i.e., FunBERT, for generating test function names. We conducted an empirical study with three industrial datasets to evaluate the effectiveness of ATAG and FunBERT. Results show that test architectures generated with ATAG (benefiting from both control and data flows) improved, on average, \(\approx \) 26–35% coupling and \(\approx \) 28–50% cohesion of the original test architectures manually constructed by test engineers from our industrial partner. FunBERT achieves 97.9%, 98.3%, and 98.1% in Precision, Recall, and F1-score, and significantly outperforms the best baseline method BERT.

Technical Debt (TD) prediction is crucial to preventing software quality degradation and maintenance cost increase. Recent Machine Learning (ML) approaches have shown promising results in TD prediction, but the imbalanced TD datasets can have a negative impact on ML model performance. Although previous TD studies have investigated various oversampling techniques that generates minority class instances to mitigate the imbalance, potentials of undersampling techniques have not yet been thoroughly explored due to the concerns about information loss. To address this gap, we investigate the impact of undersampling on TD model performance by utilizing 17,797 classes from 25 Java open-source projects. We compare the performance of the models with different undersampling techniques and evaluate the impact of combining them with widely-used oversampling techniques. Our findings reveal that (i) undersampling can significantly improve TD model performance compared to oversampling and no resampling; (ii) the combined application of undersampling and oversampling techniques leads to a synergy of further performance improvement compared to applying each technique exclusively. Based on these results, we recommend practitioners to explore various undersampling techniques and their combinations with oversampling techniques for more effective TD prediction.

Smart contracts written using the Solidity programming language of the Ethereum platform are well-known to be subject to bugs and vulnerabilities, which already have led to the loss of millions of dollars worth of assets. Since smart contract code cannot be updated to patch security flaws, reasoning about smart contract correctness to ensure the absence of vulnerabilities before their deployment is of the utmost importance. In this paper, we present a formal approach for generating correct smart contracts from B specification that verify safety properties. Our approach consists of two phases: first a smart contract and its properties are specified and verified in B, then a set of rules we defined are applied to generate the correct smart contract code in Solidity. The approach is implemented in a tool that can generate Solidity contract from a proven B project. The whole approach is demonstrated by a case study on the ERC-20 (Ethereum Request for Comments 20) Wrapped Ether (WETH) contract, which is abstractly specified in B, with invariants stating correctness properties, modeled checked with ProB for temporal properties, implemented in B0, proven correct, and automatically translated into a Solidity contract.

Maritime transportation business suffers from trust issues and burdensome paperwork. Blockchain-based smart contracts are a promising solution. Due to the nature of the blockchain, it is important to verify smart contracts before deployment, especially for its functionality and legality. In this paper, we propose a verification framework that automatically verifies the functionality and legality requirements of maritime transportation smart contracts. Smart contracts of an application, based on a set of templates, are modeled in a network of timed automata; domain-specific requirements are collected and formulated as temporal logic formulas; real-time model checking tool UPPAAL is then used to check whether these requirements are satisfied. We carry out experiments on nine real-world smart contracts to show the effectiveness and feasibility of our framework. We also compare our work with existing tools to show its effectiveness and efficiency.

The safety of modern safety-critical systems is increasingly receiving attention. AADL, as an effective modeling language, is widely used for architectural modeling of embedded safety-critical systems. Currently, the main challenges facing the safety analysis of AADL models are the system’s dynamic behavior, state space explosion, rare event prediction, and the lack of explanation of unsatisfied specifications. To address these issues, we propose QuanSafe, a discrete-time Bayesian network (DTBN)-based framework of quantitative safety analysis for AADL models. The dynamic behaviors and temporal features of AADL models can be described entirely using DTBN. Moreover, DTBN can effectively avoid state space explosion and poor performance when dealing with rare events. At the same time, DTBN has the ability of diagnostic analyses, which helps improve the system. QuanSafe provides a complete algorithm to transform AADL models into DTBN models. In addition, it supports multiple automated safety analysis methods with improved metrics. We conduct a case study on the Aircraft System. The experimental results show that our approach has higher efficiency and more comprehensive analysis capabilities than existing research.

Event-B is a refinement-based formal method that enables incremental modeling of complex systems and supports verifying system properties. Real-time systems adhere to strict timing constraints by the tasks within the system. The real-time scheduling algorithm serves as the cornerstone to guarantee the timely completion of tasks. Therefore, modeling real-time scheduling algorithms and verifying schedulability represent prominent areas of focus within the realm of real-time systems. While existing approaches often employ model checking, the scalability of the model and the problem of state explosion during verification remain challenges. Relying on theorem proving, Event-B allows for rigorous verification of system properties and circumvents state explosion. Benefiting from model refinement, the abstract model can be extended and refined to implement various scheduling algorithms.

This paper introduces an Event-B-based framework for modeling real-time scheduling algorithms and verifying properties, including schedulability. The framework provides a common refinement pattern for modeling the schedulability of the Event-B model. It facilitates the transformation of the schedulability analysis on the obtained model into the deadlock detection problem within the model. Deadlock detection can be effectively addressed through either theorem proving or model checker. We utilized Event-B to model and refine several real-time scheduling algorithms. Following the formal verification of functional and environmental requirements, we analyzed and verified the model’s schedulability within the proposed framework.

The aim of this work is to translate railML 3 files to the formal B-method to enable formal verification and validation. railML is an XML-based format designed to facilitate the exchange of information about railway systems. Our approach allows syntactic and semantic validation against predefined and custom rules, using ProB and its integrated B-Rules DSL. In addition, a B-model can be generated to animate the dynamic behaviour of the specification, which can also be used for simulations and statistical tests using SimB. A technique for creating visualisations of the topology using Graphviz is presented. Finally, real-life railML case studies show that the implemented validation process can be effectively applied to complex models and that errors in these models can be successfully detected.

We introduce a new effective way to analyze multi-threaded programs that contain self modifying code, i.e., code that modifies itself during its execution. This kind of code is widely used in malware to hide the malicious portions of their code. We introduce a new model called Self Modifying Dynamic Pushdown Network (SM-DPN) to model such programs. A SM-DPN is a network of Self-Modifying Pushdown Systems, i.e., Pushdown Systems that can modify their instructions on the fly during execution. We use finite automata to model regular infinite sets of configurations of SM-DPNs, and propose an algorithm to compute a finite automaton corresponding to the pre* reachable configurations of SM-DPNs. This allows to perform the backward reachability analysis of self modifying multi-threaded programs. We implemented our techniques in a tool and obtained encouraging results. In particular, our tool was able to detect a self-modifying multithreaded malware.

European Rail Traffic Management System (ERTMS) is a standard for the train control and signalling system whose application is spreading throughout Europe. The ETCS (European Train Control System) level 3 is attracting experts because it is still in the design phase. Many works provide formal models to the verification of ERTMS/ETCS using formal methods, but they did not investigate the validation problem. To deal with this challenge we propose an iterative formal model-driven approach that helps validating step-by-step a real formal specification of ERTMS/ETCS hybrid level 3. Our approach introduces Domain-Specific Languages (DSLs) to help system experts understand existing specifications that are already proven. To this purpose we extend and apply Meeduse, the only existing language workbench today that allows embedding formal semantics within DSLs. The paper presents this application and discusses the lessons learned from the railway and formal method experts’ points of view.

Passing the intersection is a crucial traffic scenario in urban traffic network. Rapid development of vehicle technologies makes vehicles cross the intersection more efficiently. In this paper, we propose a protocol where vehicles can pass the intersection safely and efficiently at a 6-lane dual carriageway. To ensure the safety of the protocol, we formally model the protocol and verify some necessary properties using the tool Uppaal. To evaluate the performance of our protocol, we conduct extensive experiments. After analyzing experimental data, the average rate of time reduction in a circle is over 92%. The results demonstrate that our protocol is both efficient and effective.

The use of modelling tools for the design of industrial systems is increasingly replacing the documentation production resulting from a classic system design process. One of the problems to be solved in order to fully succeed in this transition is information confidentiality management.It is also necessary to propose a system design process that allows an evolution through the whole design life cycle, and that guarantees a coherent design for a given level of confidentiality. To the best of our knowledge, neither current Model Based System Engineering (MBSE) tools, nor academic research propose solutions to this specific issue. In this paper, we propose a model based system design process to manage elements belonging to different levels of confidentiality. The process guarantees a plurality of confidentiality levels in line with Bell-Lapadula security policies for the secure management of system design and specification, as required for the protection of national and coalition defense information. It includes the separation into enclaves and adaptations guaranteeing the preservation of confidentiality and integrity to authorized users. We describe how this process can be leveraged for current modelling tools by exploiting existing multi-user functionality.

In the digital era, business collaboration platforms have become pivotal in facilitating seamless remote work and virtual team interactions. These platforms, typified by Google Workspace, offer an integrated suite of tools (such as Google Docs, Slides, and Calendar) that significantly enhance business operations. They often extend their functionality through the integration of third-party applications, known as “add-ons”. Google Workspace exemplifies this trend, blending traditional business solutions with advanced, add-on-driven capabilities. While this greatly augments productivity and collaboration for online personal or team work, concerns about the excessive use of data and permissions have been raised by both users and legislators, as add-ons can utilize the granted permissions to access and manipulate files managed by business collaboration platforms.

In the quantum computing era, the imperative role of post-quantum cryptography in securing digital communications has led to the development of computer-aided cryptography verification tools. These tools simplify the verification of post-quantum cryptography primitives and protocols, alleviating the challenges associated with manual proofs. This paper systematically reviews research in four main areas: quantum computing, post-quantum cryptography, cryptanalysis, and verification, establishing a foundation for future research. Emphasising the significance of challenges in post-quantum cryptography, we outline the current state of research on cryptography primitives and protocols. Categorising state-of-the-art computer-aided cryptography verification tools based on assumptions, models, and application levels, our analysis delves into each tool’s features, including modelling, adversary models, security properties, validation, and an in-depth analysis of their limitations. This comprehensive analysis offers insights into the nexus of post-quantum cryptography and computer-aided verification. Concluding with recommendations for researchers and practitioners, this paper explores potential future research directions.

Web frameworks play an important role in modern web applications, providing a wide range of configurations to streamline the development process. However, the intricate semantics, facilitated by framework configurations, present substantial challenges when conducting static analyses on web applications. To mitigate this issue, existing approaches resort to manually modeling framework semantics for static analysis tools. Unfortunately, these manual works are both time-consuming and error-prone, especially considering the vast array of web frameworks and their frequent updates.

In this paper, we present the first automated method for inferring web framework semantics. Our innovative approach can automatically deduce framework specifications by mutating configurations. We have developed a prototype called AutoWeb and performed extensive experiments on three popular Java web frameworks. The empirical results show that AutoWeb is comparable to these manual approaches in terms of precision, with a false negative rate of 8.2% and no false positives.

In contemporary programming languages that lack automatic memory management, such as C/C++, ensuring memory safety remains an unresolved practical challenge. Applications developed in these languages often exhibit various safety vulnerabilities. While numerous solutions have been proposed by both academia and industry, some of which have gained widespread adoption, they commonly present limitations such as the requirement for specialized hardware support, significant runtime or memory overhead, or a limited scope of problem coverage.

In this paper, we present an efficient, software-based memory safety violation mitigation scheme based on intermediate pointers and metadata embedding for the Intel x86-64 platform. The fundamental idea is to insert intermediate pointers to every pointer that points to heap memory and embed tags in the unused bits of the intermediate pointers. By inserting checks on these intermediate pointers, potential memory safety violations can be mitigated. Based on this scheme, we implement SafePtrX, a mitigation solution for heap memory safety with enhanced security properties and improved performance compared to existing methods. We also demonstrate the feasibility of SafePtrX by using publicly disclosed vulnerabilities.

A long-standing open challenge for automated program repair (APR) is search space explosion, which makes the size of the patch space too large to be handled with limited resources of time and memory. This problem is further exacerbated by the accuracy challenges of fault localization techniques, which regularly rank the actual faulty statement low on the list of suspicious statements, resulting in wasted repair effort.

This paper proposes an approach to increase the overall performance of APR for large-scale programs by utilizing parallelism for exploring the patch space, as a promising strategy to parallelize template-based APR and effectively ameliorate the accuracy challenges of fault localization. Our empirical study reveals that a substantial five-fold improvement in performance can be obtained without any degradation in repair quality. We also observe that parallelized APR produces a larger number of plausible patches than sequential APR. These encouraging results show that the proposed approach is both feasible and efficient. Future steps include investigating other promising search space splitting strategies, such as splitting based on the fix templates in template-based APR, and hybrid combinations of such strategies.