Simulation-based testing is essential for evaluating the safety of Autonomous Driving Systems (ADSs). Comprehensive evaluation requires testing across diverse scenarios that can trigger various types of violations under different conditions. While existing methods typically focus on individual diversity metrics, such as input scenarios, ADS-generated motion commands, and system violations, they often fail to capture the complex interrelationships among these elements. For instance, identical motion commands can produce different collision risks in varying scenes, and the same collision may result from different commands under different scenarios. This oversight leads to gaps in testing coverage, potentially missing critical issues in the ADS under evaluation. In this paper, we proposeCausal-Fuzzer, the first causality-aware fuzzing technique that enables efficient and comprehensive testing of ADSs by constructing causal graphs to model the interrelationships among scenarios, actions, and violations. Unlike existing methods that treat diversity metrics independently, we recognize these elements are causally interconnected and use their relationships to identify more diverse violations triggered by fundamentally different causal mechanisms. Specifically,Causal-Fuzzerproposes (1) a causality-based feedback mechanism that quantifies the combined diversity of test scenarios by assessing whether they activate new causal relationships, and (2) a causality-driven mutation strategy that prioritizes mutations on input scenario elements with higher causal impact on ego action changes and violation occurrence to enable interpretable and efficient test generation. We evaluatedCausal-Fuzzeron an industry-grade ADS Apollo, with a high-fidelity simulator LGSVL. Our empirical results demonstrate thatCausal-Fuzzersignificantly outperforms existing methods in (1) identifying a greater diversity of violations (96.5 violations on average, compared to 66.9 for the best baseline method), (2) providing enhanced testing sufficiency with improved coverage of causal relationships (13.6 unique sceneaction- violation patterns on average, compared to 8.6 for the best baseline method), and (3) achieving greater efficiency in detecting critical scenarios, strong robustness under noise conditions, and good generalizability across varying scenario complexities and violation types. Our source code and experimental results are available athttps://sites.google.com/view/causal-fuzzer.

Barrier certificate generation is an efficient and powerful technique for formally verifying safety properties of cyber-physical systems. Feed-forward neural networks (FNNs) are commonly used to synthesize barrier certificates, but the fixed activation functions limit their efficiency and scalability. In this paper, we propose a novel method for generating barrier certificates using Fourier Kolmogorov-Arnold Networks (KANs). Specifically, it utilizes Fourier KANs to replace FNNs as the template of barrier certificates. Since Fourier KAN has learnable activation functions and uses trigonometric functions as its basis functions, it can efficiently improve the representation power and is easy to train for neural barrier certificates. Then, it formally verifies the validity of the candidate Fourier KAN barrier certificates using both the Lipschitz method and the Satisfiability Modulo Theories, improving the efficiency and success rate of verification. We implement the tool KAN4BC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our method.

Ensuring the safety of autonomous driving systems (ADS) requires stress testing under diverse and complex environmental conditions. Fuzzing has emerged as a promising approach, but existing methods often neglect the interplay between map complexity and multi-object mutations, resulting in limited coverage of safety-critical behaviors. To address this gap, we propose a map-aware reinforcement learning fuzzing (MARFT) approach that adaptively tailors fuzzing actions to spatial map features while jointly mutating multiple scenario parameters. Reinforcement learning, guided by undesirable behaviors and trajectory coverage, drives the selection of fuzzing actions to maximize exposure of safety-critical events through a closed-loop cycle of “scenario state perception → fuzzing action decision → driving reward feedback”. Experimental results demonstrate that our adaptive strategy significantly outperforms non-adaptive baselines in ADS failure detection. By combining Q-learning with trajectory coverage and behavior-driven seed selection, MARFT provides a scalable and adaptive solution for ADS testing, advancing the detection of critical behavioral patterns in complex driving environments.

Control barrier certificate generation is an efficient and powerful technique for the safe control of cyber-physical systems. Feed-forward neural networks (FNNs) are commonly used to synthesize control barrier certificates and safe controllers, but they struggle to effectively address the challenges posed by high-dimensional complex systems. In this paper, we propose a novel method for generating control barrier certificates and controllers using Kolmogorov-Arnold Networks (KANs). Specifically, it utilizes KANs to replace FNNs as the template of control barrier certificates and contrllers. Since KAN has learnable activation functions, it can efficiently improve the representation power. Then, it leverages the pruning and symbolization properties of KANs, which significantly simplify the network structure, allowing for more efficient formal verification of the simplified candidate KAN control barrier certificates and controllers using Satisfiability Modulo Theories. We implement the tool KAN4CBC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate that our method addresses the issues of system dimension expansion and improved solution efficiency.

Multi-Span Question Answering (MSQA) has gained significant attention due to its relevance to real-world application scenarios. However, key information is often concentrated in small regions of the context, while large amounts of irrelevant information flood the input, leading to an excessively high proportion of negative labels, which limits the model in locating multi-span answers accurately. To alleviate this challenge, we propose two innovative methods. First, we design a text reconstruction technique for key information identification, which utilizes a multi-step information filtering mechanism to optimize the quality and structure of the input context, enabling the model to focus more on the key information relevant to questions while effectively filtering out noise interference. Second, we introduce a key information-aware joint learning framework, which jointly trains an information relevance prediction task with a multi-span answer extraction task. The framework captures the distribution patterns of key information in the context and the semantic relationships between answer spans, thereby enhancing the model’s ability to understand and reason over complex contexts. Experimental results show that the proposed approach achieves significant performance improvements on the MultiSpanQA dataset, with EM F1 improving by 3.07%-7.74% across different pre-trained language models(PLMs) compared to the current state-of-the-art(SOTA) model.

To address critical safety challenges in visionbased autonomous driving under foggy conditions, this paper proposes FOG-DETR, a trustworthy object detection framework that synergizes detection quality enhancement, system reliability assurance, and security-driven design. First, we design an Intensity-Guided Spatial Adaptive Attention Convolution (IGSAAC) mechanism to enhance feature quality by dynamically reorganizing spatial distributions, enabling precise separation of clear and fog-affected regions. Combined with a dual-path histogram self-attention strategy, our method achieves reliable feature representation through globallocal dynamic aggregation. Second, a Small Object-Enhanced Pyramid Module (SOEPM) is proposed to improve detection reliability for safety-critical small targets (e.g., pedestrians and vehicles) by integrating multi-scale features via OmniKernel fusion. The DySample module further ensures operational stability by eliminating upsampling artifacts while maintaining real-time efficiency. Experimental results on the RTTS(Rainy Traffic Testing Set) dataset demonstrate that the optimized FOGDETR achieves 2.8 % and 2.1 % improvements in mAP0.5 and mAP0.5:0.95 metrics respectively compared to the baseline RTDETR, with nearly equivalent parameter count. These advancements establish FOG-DETR as a quality-assured solution for vision systems in security-sensitive scenarios like autonomous driving and surveillance.

Ensuring the safety of autonomous driving systems (ADSs) is essential, which requires effective testing methods to enhance system robustness. Fuzz testing (FT) is a widely used technique for uncovering software faults by generating test cases that trigger unexpected system behaviors. However, traditional FT in ADS suffers from significant limitations, including inefficient seed selection, low test case relevance, and inadequate exploration of diverse failure‐inducing driving scenarios. Random fuzzing often yields redundant or ineffective cases, limiting the detection of safety‐critical issues. To address these challenges, we propose ReinSeed, a reinforcement FT (RFT) framework that integrates three key phases: prefuzzing seed optimization, reinforcement learning (RL)–based scenario generation, and postfuzzing seed prioritization. We introduce a scenario complexity index to prioritize initial seeds before fuzzing. During fuzzing, we model the process as a Markov decision process (MDP) and apply Q ‐learning to generate scenarios with effective fuzzing action variations guided by driving behaviors, including undesired behaviors and trajectory coverage. To further improve testing effectiveness, we present a postfuzzing prioritization strategy that ranks fuzzed scenarios based on risk energy by incorporating control constraint violation analysis, safety‐critical events, and risk‐driven trajectory. Experimental results demonstrate that the unified framework—ReinSeed—significantly improves the detection of undesired behaviors, outperforming baseline methods across maps of varying complexity. Furthermore, the multiphase seed optimization showcases distinct contributions of scenario complexity, behavior‐guided fuzzing, and risk energy in enhancing both the efficiency and effectiveness of discovering critical behaviors in ADS.

ABSTRACT Understanding the evolution of software systems is crucial for advancing software engineering practices. Many studies have been devoted to exploring software evolution. However, they primarily treat software as an entire entity and overlook the inherent differences between subsystems, which may lead to biased conclusions. In this study, we attempt to explore variations between subsystems by investigating the code feature differences between kernel and nonkernel components from an evolutionary perspective. Based on three operating systems as case studies, we examine multiple dimensions, including the code churn characteristics and code inherent characteristics. The main findings are as follows: (1) The proportion of kernel code remains relatively small, and exhibits consistent stability across the majority of versions as systems evolve. (2) Kernel code exhibits higher stability in contrast to nonkernel code, characterized by a lower modification rate and finer modification granularity. The patterns of modification activities are similar in both kernel and nonkernel code, with a preference of changing code and a tendency to avoid the combination of adding and deleting code. (3) The cumulative code size and complexity of kernel files show an upward trajectory as the system evolves. (4) Kernel files exhibit a significantly higher code density and complexity than nonkernel files, featuring a greater number of code line, comments, and statements, along with a larger program length, vocabulary, and volume. Conversely, kernel functions prioritize modularity and maintainability, with a significantly smaller size and lower complexity than nonkernel functions. These insights contribute to a deeper understanding of the dynamics within operating system codebases and highlight the necessity of targeted maintenance strategies for different subsystems.

Barrier certificate generation is an ingenious and powerful approach for safety verification of cyber-physical systems. This article suggests a new learning and verification framework that helps to achieve the balance between the representation ability and the verification efficiency for neural barrier certificates. In the learning phase, it learns candidate barrier certificates represented as convex difference neural networks (CDiNNs). Since CDiNNs can be rewritten as difference of convex (DC) functions that can express any twice differentiable function, thus have outstanding representation ability and flexibility. In the verification phase, it employs an efficient approach for formally verifying the validity of the neural candidates via DC programming. Due to the convexity-based structure, CDiNNs can significantly facilitate the verification process. We conduct an experimental evaluation over a set of benchmarks, which validates that our method is much more efficient and effective than the state-of-the-art approaches.

Information leakage easily occurs in large-scale information interactions and brings harm to individuals, enterprises, and society. As a well-known security policy, Chinese Wall (CW) provides a security guideline, which combines mandatory and discretionary access control to avoid information leakage. Colored Petri nets (CPNs) are a widely used formal method, well suited for verification of CW policy due to the capability of characterizing the concurrency. However, CPN easily suffers from the problem of state space explosion due to the interleaving semantics. The unfolding techniques can effectively alleviate this problem. In this article, we apply simplified CPN and their unfolding techniques to detect information leakage against CW policy. Specifically, we define a CPN-based CW model, propose an algorithm to generate the merged process of CPN, and detect the potential information leakage by analyzing the structural behaviors of its unfoldings. Furthermore, we conduct a case study and several experiments to show the advantages of our method. The results exhibit that our method can effectively detect information leakage against CW policy and alleviate the state space explosion.

Trusted Execution Environment (TEE) provides isolation for sensitive data in electronic devices and its compromise can lead to enormous losses. TEE's information-flow security is essential and can be robustly ensured by formal methods. Nevertheless, the cross-domain API invocation of TEE is intricate for information-flow analysis, and the service provider on the TEE, i.e., trusted application, brings complexity to the TEE specification and verification. Existing research seldom delves into general TEEs that are compliant with GlobalPlatform (GP), which is an important and universal TEE standard. Furthermore, they do not align with the requirements for Common Criteria certification. In this paper, we propose a TEE-applicable and Common Criteria-oriented framework to specify and verify the information-flow security of GP TEE, which is applied to the verification of the real-world commercial MiTEE. Firstly, we present a framework for TEE that aligns with the requirements of Common Criteria's highest assurance level (EAL 7). It incorporates a domainswitch based mechanism to model the cross-domain TEE API invocation and a parameterized modeling approach to handle trusted applications. Secondly, we model GlobalPlatform-compliant TEE with the framework as GP TEE security model layer and function layer, which are reusable for all GP TEEs. Thirdly, we specify MiTEE as the MiTEE design layer that refines GP TEE model. Lastly, we verify the information-flow security of GP TEE and MiTEE via theorem proving and uncover four critical vulnerabilities in MiTEE. This work contributes to MiTEE's acquirement of an EAL 5+ certificate. All works are carried out in Isabelle/HOL, with nearly 32000 lines of code.

Control barrier certificate is an ingenious and practical approach of safety controller synthesis for cyber-physical systems. In this article, we present an approach for synthesizing safety controllers for controlled discrete-time systems subject to safety constraints. We first introduce a new type of$k$-inductive control barrier certificates ($k$-ICBCs), which relaxes the strict nonincreasing condition of general control barrier certificates. Apart from this, we propose a certificate synthesis framework that includes a learner and a verifier. They collaborate continuously to search for safety controllers and their corresponding$k$-ICBCs simultaneously. The learner obtains neural controllers and candidate$k$-ICBCs through supervised learning, while the verifier addresses a series of mixed integer linear programming problems to validate the candidate$k$-ICBCs or provide counterexamples to guide the learner further. Thanks to the less conservatism of$k$-inductive conditions, safety neural controllers, and$k$-ICBCs can be easily and quickly obtained. We showcase through benchmark examples that our method is efficient, and$k$-inductive conditions can improve the effectiveness of control barrier certificate synthesis methods by successfully verifying systems that are challenging to handle with general control barrier certificate conditions.

Formal synthesis of safe controllers is essential for safety-critical cyber-physical systems. In this paper, we propose a novel counterexample guided approach for synthesizing safe controllers of nonlinear systems using Bayesian optimization enhanced reinforcement learning, to improve the efficiency of the training process while ensuring safety property. First, we utilize the control barrier function technique to establish a constrained Markov decision process, which enables us to learn an initial controller with minimal safety violations. We then design a counterexample guided policy refinement using Bayesian optimization, to fine-tune the initial controller based on the failure trajectories. Finally, we suggest a compensatory mechanism to correct the tuned controller to guarantee the safety property. We implement the CEGRLPR tool and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our approach.

Named entity recognition is the most basic task in natural language processing, and its quality directly affects the performance of downstream tasks. Due to the scarcity of annotated corpus and diverse species in the medical domain, as well as the continuous emergence of neologisms, the application of general domain entity recognition methods in vertical fields face the problem of inaccurate recognition of professional vocabulary. Proximity relation as a strong prior information is of great significance for the annotation task of named entity recognition. In view of the insufficient of proximity modeling in current work, we propose a named entity recognition model based on proximity relationship enhancement (PEM). Firstly, BERT is introduced to obtain the semantic features of text sequences. At the same time, the embedding vectors corresponding to lexical labels and co-occurrence matrices are input into the graph attention network. This network uses an information gate mechanism to model the proximity dependencies and filter the redundant features. Furtherly, we utilize the multi-head cross attention mechanisms to align and fuse the proximity features, and introduce BiLSTM to extract the contextual semantics. Finally, the fused features are fed into CRF for decoding. In order to verify the effectiveness of the model in this paper, comparative ablation experiments are carried out on four commonly used medical entity datasets, such as CCKS2018. The experimental results further demonstrate that the PEM model outperforms other recognition models and can effectively improve the accuracy of entity recognition with good robustness.

Social network texts contain a great deal of sentiment information. Such information reflects the personal attitudes and emotional dispositions for particular topics or events. However, not much comprehensive semantic information and not enough text data are used by traditional text sentiment analysis models, consequently, there are shortcomings in the analysis results. To handle this problem, in this paper, we propose a text sentiment analysis model NBWAB based on BERT-WWM-ATT-BiLSTM text classification. Our optimal model is constructed as follows. BERT-WWM is first used to dynamically encode the character-level and sentence-level features, and then Bi-LSTM is used to capture deeper semantic features of texts. Finally, these results are fused with the relevant multi-dimensional features of texts by multi-head-attention feature fusion skill. To further improve the performance of text sentiment analysis, we employ the ChatGPT data augmentation method to extend training datasets. To show the efficiency of our model, we have conducted experiments on three Chinese datasets: SMP2020-EWECT, Waimai_10k, and Weibo_senti_100k. The accuracy and F1 value of the model on the SMP2020-EWECT dataset (usual) are 80.76% and 77.61%, respectively, the accuracy and F1 value on the Waimai_10k dataset are 92.29% and 91.34%, respectively, and the accuracy and F1 value on the Weibo_senti_100k dataset are 98.10% and 98.24%, respectively. The results show that our model has advantages over the existing models in that more semantic information and more text data are considered for text analysis.

Model-based Test Case Prioritization utilizing similarity metrics has proved effective in software testing. However, the utility of similarity metrics in it varies with test scenarios, hindering its universal effectiveness and performance optimization . To tackle this problem, we propose a Diversity-driven Learn-to-rank model-based TCP approach, named DLTCP, for optimizing early fault detection performance. Our method first employs the whale optimization algorithm to search for a suitable set of similarity metrics from a pool of existing candidates. This search process determines which metrics should be used. According to each selected metric, test cases are then prioritized. The resulting test case rankings are used as the training data for DLTCP. Finally, the proposed method incorporates random forest to train a ranking model for test case prioritization. As such, it can fuse multiple similarity metrics to improve the TCP performance. We conduct extensive experiments to evaluate our method’s performance using the average percentage fault detected (APFD) as metric. The experimental results show that DLTCP achieve an average APFD value of 0.953 for seven classic benchmark models , which is 11.37% higher than that of the state-of-the-art algorithms. It can well select a set of similarity metrics for effective fusion, demonstrating competitive performance in early fault detection.

Industrial operating systems (IOS) are essential for supporting smart manufacturing, particularly in managing and utilizing heterogeneous production resources through resource instantiation scheduling (RIS) technique. However, RIS faces the challenge of efficiently selecting optimal resource service compositions from numerous options with varying quality of service . To boost the solving of the RIS problem and improve the quality of the solution, this paper proposes a novel hybrid algorithm, named DWOA, based on the whale optimization algorithm (WOA) and deep reinforcement learning (DRL). It first incorporates the DRL algorithm to learn experience from the historical data regarding exploration and exploitation in the WOA search process and train an optimal behavior decision model. Subsequently, utilizing the trained model, the DWOA can effectively guide the search agent in achieving a better balance between global exploration and local exploitation, thereby enhancing its convergence speed and solution quality. The effectiveness and efficiency of the DWOA approach are evaluated by the CEC2017 benchmark functions and RIS problems with various scales, compared with 11 state-of-the-art methods. The experimental results indicate that our method converges faster and produces better solutions for RIS problems.

Synchronous Dataflow graphs (SDFGs) are widely used to model streaming applications that exhibit data-driven and iterative execution patterns. Graph conversion techniques such as retiming, unfolding, and pipelining are commonly used to optimize the iteration periods (IPs) of SDFGs. In this paper, we propose an extension of the graph conversion based pipelining approach for single-rate SDFGs to multi-rate SDFGs. A new perspective on pipelining is introduced, where the pipelining of a general-time SDFG can be viewed as the retiming of a unit-time SDFG. Based on this perspective, we prove that optimal pipelining can always achieve an IP less than 1 time unit longer than the optimal IP for an SDFG. Furthermore, an efficient optimal SDFG pipelining algorithm called GCP-SDFG is presented. Experimental results show that GCP-SDFG has significant advantages in IP minimizing and runtime relative to three state-of-the-art retiming or pipelining algorithms.

Deep reinforcement learning (DRL) is widely applied in motion planning for multi-robot systems as DRL leverages the offline training process to improve the real-time computation efficiency. In DRL-based methods, the DRL models compute an action for a robot based on the states of its surrounding obstacles, including other robots in the system. They always assume that the number of obstacles is fixed and the obtained obstacles’ states are reliable. However, in the real world, a multi-robot system may suffer from various attacks, such as remote control attacks and network attacks, that cause wrong positions of the surrounding obstacles received by a robot. In this paper, we propose a robust motion planning methodDAE-Crit-LSTM, integrating a denoising autoencoder (DAE) with DRL models, to mitigate such position deception attacks in environments with a different number of obstacles.DAE-Crit-LSTMshows the following two advantages. First,DAE-Crit-LSTMcan be applied in benign and attacked scenarios and thus does not require any detector. It learns an encoder and a decoder to approximate the accurate positions of the obstacles, no matter under attack or not. Second,DAE-Crit-LSTMapplies an LSTM (Long Short-Term Memory)-based DRL model to deal with a variable number of obstacles in the environment. It is worth noting thatDAE-Crit-LSTMis method-agnostic and can be easily implemented in state-of-the-art motion planning methods. Comprehensive experiments show thatDAE-Crit-LSTMcan mitigate position deception attacks and guarantee safe motion. We also demonstrate the effectiveness and generalization ofDAE-Crit-LSTM.

Machine learning has become a promising technology for anomaly detection of cyber-physical systems (CPSs). However, the trained anomaly detection models always suffer from bias due to the scarcity of anomaly data in CPSs and the biased data collection process, which may poison the models' generalization ability. Recent debiasing methods are proposed to deal with the bias via resampling the training dataset, reweighting during the training phase, or adjusting the classification threshold. However, they may lose valuable information, need extra knowledge of the models, or lead to overfitting. Especially, they lack a causal understanding of the debiasing process, so they cannot point out the source and propagation of the bias and, thus, cannot deal with it in an explainable way. In this article, we propose a counterfactual debiasing framework to mitigate the bias in a well-trained model. First, we formalize the model's training and inference processes using causal graphs. Thus, we can understand the source and propagation of the model's bias through causal inference. Then, we use counterfactual inference to estimate the bias's detrimental causal effect on the prediction and remove it from the total causal effect. Therefore, we can conduct unbiased inferences with a biased model. The proposed method can remove the bias in an explainable way by incorporating causal graphs. Comprehensive experiments are conducted on seven real-world CPS datasets, i.e., IDA, MFP, ACS, SPF, UNS, NSL, and ICS. The results demonstrate the effectiveness, compatibility, and unbiasedness of the proposed approach.

Distributed motion control is critical in multiple mobile robot systems (MMRSs). Current research usually focuses on either discrete approaches, which aim to deal with high-level collisions and deadlocks without considering the low-level motion commands, or continuous approaches, which can optimize low-level continuous commands to mobile robots but cannot deal with deadlocks efficiently. In this article, by combining discrete and continuous methods, we design a hybrid motion control method for MMRSs where each robot should move along a predefined path. First, each robot’s motion is modeled as a discrete transition system, based on which a real-time supervisory control policy is illustrated to avoid collisions and deadlocks. Second, according to the discrete decisions, the continuous speed at each discrete state is computed using model predictive control and sequential convex programming. The proposed hybrid approach brings two advantages. First, the discrete control component guarantees collision and deadlock avoidance and reduces the scale of the optimization problems. Second, continuous control optimizes the continuous speed in real time and fulfills other performance requirements like time and energy costs. To move in a fully distributed way, each robot needs to predict the motion of its neighbors by retrieving their immediately available information through communications. The simulation and real-world experimental results show the effectiveness of our approach.

Background: Bug dependencies refer to the link relationships between bugs and related issues, which are commonly observed in software evolution. It has been found that bugs with bug dependencies often take longer time to be resolved than other bugs without any dependencies. Despite the potential impact of bug dependencies on bug-fixing time, previous studies use traditional metrics without considering bug dependencies to build bug-fixing time prediction models. As a result, there is currently little empirical evidence to support the use of bug dependencies in improving prediction accuracy. Aims: We aim to conduct a comprehensive empirical study to investigate the value of considering bug dependencies for bug-fixing time prediction. Method: We define a set of bug dependency metrics based on bug dependencies. We first investigate the correlation between bug dependency metrics and bug-fixing time to investigate whether bugs with more complex dependencies are more time-consuming to be fixed. Next, we employ principal component analysis to study whether bug dependency metrics capture additional dimensions of a bug compared to traditional metrics. Finally, we build multivariate prediction models to explore whether considering bug dependencies can improve the effectiveness of bug-fixing time prediction. Results: The experimental results suggest that: (1) bugs with more complex dependencies require more time to be fixed; (2) bug dependency metrics are complementary to traditional metrics; (3) considering bug dependencies can improve the effectiveness of bug-fixing time prediction. Conclusions: These findings highlight the importance of considering bug dependencies in bug-fixing time prediction, and provide valuable insights into the potential impact of bug dependencies on software development processes.

Due to the prevalent application of machine learning (ML) techniques and the intrinsic black-box nature of ML models, the need for good explanations that are sufficient and necessary towards a model’s prediction has been well recognized and emphasized. Existing explanation approaches, however, favor either the sufficiency or necessity. To fill this gap, we present DDImage, a technique and tool that automatically produces explanations preserving dual properties for ML-based image classifiers. The core idea behind DDImage is to discover an appropriate explanation by debugging the given input image via a series of image reductions, with respect to the sufficiency and necessity properties. We conduct comprehensive experiments to compare our approach against two state-of-the-art approaches, BayLIME and SEDC, on widely-used models and datasets. The results show that our approach outperforms the other methods in producing minimal explanations preserving both sufficiency and necessity, and it matches or exceeds the other methods in terms of stability.

Recent advances of consensus control have made it significant in multi-agent systems such as in distributed machine learning, distributed multi-vehicle cooperative systems. However, during its application it is crucial to achieve resilience and privacy; specifically, when there are adversary/faulty nodes in a general topology structure, normal agents can also reach consensus while keeping their actual states unobserved. In this article, we modify the state-of-the-art Q-consensus algorithm by introducing predefined noise or well-designed cryptography to guarantee the privacy of each agent state. In the former case, we add specified noise on agent state before it is transmitted to the neighbors and then gradually decrease the value of noise so the exact agent state cannot be evaluated. In the latter one, the Paillier cryptosystem is applied for reconstructing reward function in two consecutive interactions between each pair of neighboring agents. Therefore, multi-agent privacy-preserving resilient consensus (MAPPRC) can be achieved in a general topology structure. Moreover, in the modified version, we reconstruct reward function and credibility function so both convergence rate and stability of the system are improved. The simulation results indicate the algorithms’ tolerance for constant and/or persistent faulty agents as well as their protection of privacy. Compared with the previous studies that consider both resilience and privacy-preserving requirements, the proposed algorithms in this article greatly relax the topological conditions. At the end of the article, to verify the effectiveness of the proposed algorithms, we conduct two sets of experiments, i.e., a smart-car hardware platform consisting of four vehicles and a distributed machine learning platform containing 10 workers and a server.

Barrier certificate is a powerful and practical approach of safety verification for hybrid systems. In this paper, we propose a novel Counterexample-Guided Inductive Synthesis (CEGIS) procedure for synthesizing neural barrier certificates. The CEGIS procedure is structured as an inductive loop where a learner and a verifier interact to synthesize barrier certificates. The learner trains candidate barrier certificates expressed as feedforward neural networks with polynomial activations, and the verifier employs computer algebra techniques to either ensure the validity of the trained candidate barrier certificate or produce informative counterexamples, which can effectively reduce the number of CEGIS iterations. We implement the CEGIS tool and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our approach.

Graphical User Interface (GUI) has become one of the most effective human-computer communication medium today. The quality of GUI is essential to the success of apps, especially for mobile apps. Developers not only have to understand the interaction of various components, but also follow the principles of design and implementation. It is helpful for developers to understand the challenges via analyzing the questions and answers (Q&A) on GUI development. However, there is no large-scale study on the GUI development posts on Stack Overflow. In this paper, we conduct an exploratory study on 23,741 posts related to GUI development on Stack Overflow. We first extract 20 topics related to GUI development using topic modeling. After manually classifying these GUI topics into 5 categories, we further quantitatively analyze the popularity and difficulty of GUI topics, the correlation between these two aspects, and qualitatively analyze the distribution of question types in posts. Finally, we have some interesting findings. These findings contain that the topic "tool selection" is the most popular topic, the topic "thread" has the highest percentage of unaccepted answers, and the topic "client/server" answer takes the longest time to be accepted. In addition, we discuss about possible inspirations of our research to GUI development stakeholders.

Software refactoring is one of the most significant practices in software maintenance as the quality of software design tends to deteriorate during software evolution. But, refactoring software is a very challenging task as it requires a holistic view of the entire software system. To this end, recent studies introduced search-based algorithms to facilitate software refactoring. However, they still have the following major limitations: 1) the searched solutions may violate the design principles as their fitness functions do not directly reflect the degree of software’s compliance with design principles; 2) most approaches start the searching process from a completely random initial population, which may lead to unoptimal solutions. In this article, we aim to develop effective search-based refactoring approach to recommend better refactoring activities for developers which can improve the degree of software’s compliance with design principles as well as the software design quality. We proposeDEPICTER, a design-principle guided and heuristic-rule constrained software refactoring recommendation approach. In particular,DEPICTERuses non-dominated sorting genetic algorithm (NSGA)-II genetic algorithm and employs design-principle metrics as fitness functions. Besides,DEPICTERleverages heuristic rules to improve the quality of initial population for subsequent generic evolution. Our evaluations, based on four widely used systems, show thatDEPICTERis effective for guiding the development of better refactoring models in practice.

With the plain text descriptions of design patterns, developers could better learn and understand the definitions and usage scenarios of design patterns. To facilitate the automatic usage of these descriptions, e.g., recommending design patterns by free-text queries, design patterns and natural languages should be adequately associated. Existing studies usually use texts in design pattern books as the representations of design patterns to calculate similarities with the queries. However, this way is problematic. Lots of information of design patterns may be absent from design pattern books and many words would be out of vocabulary due to the content limitation of these books. To overcome these issues, a more comprehensive method should be constructed to estimate the relatedness between design patterns and natural language words. Motivated by Word2Vec, in this study, we propose DPWord2Vec that embeds design patterns and natural language words into vectors simultaneously. We first build a corpus containing more than 400 thousand documents extracted from design pattern books, Wikipedia, and Stack Overflow. Next, we redefine the concept of context window to associate design patterns with words. Then, the design pattern and word vector representations are learnt by leveraging an advanced word embedding method. The learnt design pattern and word vectors can be universally used in textual description based design pattern tasks. An evaluation shows that DPWord2Vec outperforms the baseline algorithms by 24.2-120.9 percent in measuring the similarities between design patterns and words in terms of Spearman’s rank correlation coefficient. Moreover, we adopt DPWord2Vec on two typical design pattern tasks. In the design pattern tag recommendation task, the DPWord2Vec-based method outperforms two state-of-the-art algorithms by 6.6 and 32.7 percent respectively when considering$Recall@10$. In the design pattern selection task, DPWord2Vec improves the existing methods by 6.5-70.7 percent in terms of MRR.

Natural language inference (NLI) is a fundamental NLP task that forms the cornerstone of deep natural language understanding. Unfortunately, evaluation of NLI models is challenging. On one hand, due to the lack of test oracles, it is difficult to automatically judge the correctness of NLI's prediction results. On the other hand, apart from knowing how well a model performs, there is a further need for understanding the capabilities and characteristics of different NLI models. To mitigate these issues, we propose to apply the technique of metamorphic testing (MT) to NLI. We identify six categories of metamorphic relations, covering a wide range of properties that are expected to be possessed by NLI task. Based on this, MT can be conducted on NLI models without using test oracles, and MT results are able to interpret NLI models' capabilities from varying aspects. We further demonstrate the validity and effectiveness of our approach by conducting experiments on five NLI models. Our experiments expose a large number of prediction failures from subject NLI models, and also yield interpretations for common characteristics of NLI models.

Test-suite-based automated program repair (APR) techniques acquire information from an input test suite to guide the repair process, aiming to produce a repair that can pass all test cases of the input test suite. Obviously, the input test suite has a critical impact on the repair effectiveness of APR techniques. This article reports on a study of the APR input test suites from a new perspective. We first propose a novel method of constructing the APR input test suites, using information derived from violated metamorphic relations. We then empirically evaluate our construction method using three APR techniques (Angelix, CETI, and GenProg), comparing it with random and code-coverage-based construction methods that are used as the experimental control. The results show that our approach is complementary to these two input test suite construction methods. This article illustrates a new use of metamorphic relations for program repair.

During flights, an unmanned aerial vehicle (UAV) may not be allowed to move across certain areas due to soft constraints such as privacy restrictions. Current methods on self-adaption focus mostly on motion planning such that the trajectory does not trespass predetermined restricted areas. When the environment is cluttered with uncertain obstacles, however, these motion planning algorithms are not flexible enough to find a trajectory that satisfies additional privacy-preserving requirements within a tight time budget during the flights. In this paper, we propose a privacy risk aware motion planning method through the reconfiguration of privacy-sensitive sensors. It minimises environmental impact by re-configuring the sensor during flight, while still guaranteeing the safety and energy hard constraints such as collision avoidance and timeliness. First, we formulate a model for assessing privacy risks of dynamically detected restricted areas. In case the UAV cannot find a feasible solution to satisfy both hard and soft constraints from the current configuration, our decision making method can then produce an optimal reconfiguration of the privacy-sensitive sensor with a more efficient trajectory. We evaluate the proposal through various simulations with different settings in a virtual environment and also validate the approach through real test flights on DJI Matrice 100 UAV.

Code search engines are widely used by software developers. However, due to the huge amount of data being processed as well as the lack of complete specifications, the testing of code search engines faces the oracle problem. Metamorphic testing (MT) is a well-known testing technique that is effective for alleviating the oracle problem. In this paper, we propose to apply MT to test code search engines. We first identify five metamorphic relations (MRs) by considering the characteristics of code search engines. Four MRs are defined based on the partial specifications of code search engines and thus are used for the purpose of verification, and the one MR identified from the users' perspective can be used to conduct validation. The approach is evaluated by conducting a series of experiments involving four popular code search engines (namely, Krugle, searchcode, sourcegraph and Zoekt), and one well-known code repository (namely, GitHub) that provides the code search services. The experimental results show that the abnormal behaviors of Krugle, searchcode, GitHub, and Zoekt have been successfully detected. By further inspecting the root causes of these abnormal behaviors, three critical issues related with the code search engines under investigation are identified and reported. These results demonstrate the effectiveness of our approach, and are also helpful for the users and developers to gain a deeper understanding about the code search engines.

In recent years, tracking a ground moving target with an unmanned aerial vehicle (UAV) has played a key role in navigation, military reconnaissance, field rescue, and traffic monitoring tasks. However, due to the maneuvering uncertainty of the moving target and various uncertainties in the complex environment, it has brought many difficulties to the tracking task. In this paper, aiming at addressing the various uncertainties in the process of target tracking with UAV, we present a control strategy based on interval type-2 fuzzy logic. We design two interval type-2 fuzzy controllers to control the yaw angle and speed of the UAV, respectively. Images obtained from an embedded camera on the UAV platform are visually processed by the target recognition and tracking algorithms in the early stage to detect the pixel position of the target in every frame, which is used as the input of the controller we have designed. Through the analysis of the input and output data of controllers designed by us and the analysis of the tracking error, the reliability of control strategy proposed by us is proved. At last, a series of simulation experiments are implemented in ROS to demonstrate the performance of the target-tracking strategy we proposed.

Motion planning is one of the most critical problems in multirobot systems. The basic target is to generate a collision-free trajectory for each robot from its initial position to the target position. In this paper, we study the trajectory planning for the multirobot systems operating in unstructured and changing environments. Each robot is equipped with some sensors of limited sensing ranges. We propose a fully distributed approach to planning trajectories for such systems. It combines the model predictive control (MPC) strategy and the incremental sequential convex programming (iSCP) method. The MPC framework is applied to detect the local running environment real-timely with the concept of receding horizon. For each robot, a nonlinear programming is built in its current prediction horizon. To construct its own optimization problem, a robot first needs to communicate with its neighbors to retrieve their current states. Then, the robot predicts the neighbors' future positions in the current horizon and constructs the problem without waiting for the prediction information from its neighbors. At last, each robot solves its problem independently via the iSCP method such that the robot can move autonomously. The proposed method is polynomial in its computational complexity.

A self-adaptive software system is one that can autonomously modify its behavior at runtime in response to changes in the system and its environment. It is a challenge to model such a kind of systems since it is hard to predict runtime environmental changes at the design phase. In this paper, a formal model called intelligent Petri net (I-PN) is proposed to model a self-adaptive software system. I-PN is formed by incorporating fuzzy rules to a regular Petri net. The proposed net has the following advantages. 1) Since fuzzy rules can express the behavior of a system in an interpretable way and their variables can be reconfigured by the runtime data, the proposed model can model runtime environment and system behavior. 2) Since a fuzzy inference system with well-defined semantics can be used in a complementary way with other model languages for the analysis, thus the proposed model can be analyzed, even though it is described in two different languages: component behaviors in Petri nets while logic control in fuzzy rules. 3) The proposed model has self-adaption ability and can make adaptive decisions at runtime with the help of fuzzy inference reasoning. We adopt a manufacturing system to show the feasibility of the proposed model.

Nowadays, software systems have been more and more complex, which causes great challenges to maintain the availability of the systems. Online failure prediction provides an effective approach to guaranteeing the validity of the systems. Most of the current technologies for online failure prediction require some prior knowledge, such as the model of the system or failure patterns. This paper proposes a new method based on fuzzy rules and time series analysis. Specifically, fuzzy rules are used to model the relationships among different variables, whereas univariate time series analysis is used to describe the evolution of each variable. Thus, for a dependent variable, we have two predicted values: one is from the time series model, and the other is computed from fuzzy rules with fuzzy inference. If the difference between the two values exceeds a threshold, then we declare that there would be a failure in some time period ahead. Different from the existing methods, the proposed method considers not only the evolutionary trend of each variable but also the relationships among different variables. Moreover, we do not need any prior knowledge such as system model or failure patterns. We use a railway transportation system as an example to illustrate our method.

Concurrency bug detection is a time-consuming activity in the debugging process for concurrent programs. Existing techniques mainly focus on detecting data race bugs with pattern analysis; however, the number of interleaving patterns could be huge, only the most suspicious write-read pattern is given, and an oracle is needed, which is not available in the operational phase. This paper proposes a program-invariant-based technique to detect a class of concurrent program bugs. By unit testing of the components of a concurrent program, we obtain a set of program invariants, which can be used as an oracle to obtain “bad” invariants when the program is online. By using the function call graph of the components and applying a reduction technique to the invariants, we find the candidates of suspicious functions and rank them. From the interactions among components, we analyze the causes to the concurrency bugs. Experimental results show that our proposed technique is effective in concurrency bug detection.

Collision avoidance is a critical problem in motion planning and control of multirobot systems. Moreover, it may induce deadlocks during the procedure to avoid collisions. In this paper, we study the motion control of multirobot systems where each robot has its own predetermined and closed path to execute persistent motion. We propose a real-time and distributed algorithm for both collision and deadlock avoidance by repeatedly stopping and resuming robots. The motion of each robot is first modeled as a labeled transition system, and then controlled by a distributed algorithm to avoid collisions and deadlocks. Each robot can execute the algorithm autonomously and real-timely by checking whether its succeeding state is occupied and whether the one-step move can cause deadlocks. Performance analysis of the proposed algorithm is also conducted. The conclusion is that the algorithm is not only practically operative but also maximally permissive. A set of simulations for a system with four robots are carried out in MATLAB. The results also validate the effectiveness of our algorithm.

Software architecture forms a bridge between requirements and code. In this paper, by defining port operations, we use port activities to describe component-based software architectures. We can get the following benefits: 1) The representation of an architecture with the proposed formulism is simpler comparing with those by other ADLs. 2) An architecture is a semigroup to the component operations: composing and nesting. This result may be used to check the consistence and adaptability of two architectures. 3) The port expressions can be easily mapped to Petri net, so that the port-based process can be checked through the analysis of the Petri nets.

A software system's requirements are often specified by textual use cases due to the latter's concrete and narrative style of expressions. However, they have limitation in the synthesis of the system behavior since they have a poor basis for the formal interpretation. Existing synthesis techniques are either largely manual or focus on the use case interactions. We present a framework from a model-based point of view to automatically synthesize system behavior from textual use cases to a Petri net model. The generated net model can well describe component module interactions and thus can be used to check the requirement properties. The function of Send-Railway-Emergency-Call of European Integrated Railway Radio Enhanced Network is used to show the proposed method. Moreover, the experimental results on a set of examples demonstrate the effectiveness of the proposed method.

Reliability is an important metric for measuring the quality of software. Many methods have been proposed for online predicting and improving software reliability, but most of them have the following weakness: they are not able to predict software reliability on different time intervals and to locate the faulty components that cause the declining of the reliability either. This paper proposes a new method for online improvement of reliability of service composition. We use monitored failure data at ports of services to predict the reliabilities of service composition on different time intervals. If the predicted reliability is lower than the expected value, then we locate the faulty components that cause the declining of the reliability by using an improved spectrum-fault-localization (SFL) technique. The system can be automatically reconfigured to improve the system reliability by adding a component replica or replacing the faulty component. An Online Shop example is used to demonstrate the effectiveness of our method.

Traditional models unable to model adaptive software systems since they deal with fixed requirements only, but cannot handle the behaviors that change at runtime in response to environmental changes. In this paper, an adaptive Petri net (APN) is proposed to model a self-adaptive software system. It is an extension of hybrid Petri nets by embedding a neural network algorithm into them at some special transitions. The proposed net has the following advantages: 1) it can model a runtime environment; 2) the components in the model can collaborate to make adaption decisions while the system is running; and 3) the computation is done at the local component, while the adaption is for the whole system. We illustrate the proposed APN by modeling a manufacturing system.

In this paper, a new method is proposed to evaluate the performance of concurrent systems. A concurrent system consisting of multiple processes that communicate via message passing mechanisms is modeled by a Petri net, which is in turn represented by a set of ordinary differential equations (ODEs) of a restricted type. The equations describe the system state changes, and the solutions, also called state measures, can be used for the performance analysis such as estimating response time, throughput and efficiency. This method can avoid a state explosion problem encountered by the conventional methods based on Continuous-Time Markov Chains. Its application to an IBM business system is given as an example.

Switched stochastic systems (SSS) can be used to describe hybrid systems with randomness. However, the languages to describe their discrete switching logic and stochastic dynamic processes are different, and this difference makes their design and analysis hard. This paper proposes a new Petri net model, namely stochastic-differential Petri net (S-DPN), to describe both discrete switching logic, represented by a Markov chain, and stochastic dynamic processes, represented by a set of stochastic differential equations. We then apply a model checking technique to S-DPN to check the correctness of the requirements of SSS. A temperature control system is used to demonstrate the effectiveness of our method.

Switched fuzzy systems can be used to describe the hybrid systems with fuzziness. Their stability issue is the most important one and has received significant attention. Most of the existing methods to study it are based on Lyapunov functions. However, the existence of such functions is difficult to establish. This paper presents a new method to analyze the stability. A switched fuzzy system with a Takagi–Sugeno (T–S) fuzzy model is first transformed to a hybrid automaton (HA) that is linearized. The reachability of this linearized one is then checked by the model checker PHAVer. Finally, the stability is obtained by analyzing the reachability. It is shown that a switched fuzzy system and its corresponding HA have the same behavior and that the linearization does not affect the stability analysis. We demonstrate the effectiveness of our method through a case study on a differential-drive two-wheeled mobile robot.

Deadlock detection for concurrent systems via static analysis is in general difficult because of state-space explosion; indeed it is PSPACE compete. This paper presents a new method to detect the deadlocks. A concurrent system consisting of several processes that communicate using a resource sharing mechanism is represented by a set of ordinary differential equations of a restricted type. The equations describe the system state changes, and their solutions, also called state measures, indicate the extent to which the state can be reached in execution. Based on the solutions, the resource deadlock can be detected. By taking into account the computation errors of numerical solution for the differential equations, the detection can be performed via a MATLAB solver, as shown in the experiments. The complexity of the proposed method is polynomial.

The Clock Constraint Specification Language (CCSL) is a formal polychronous language based on the notion of logical clock. It defines a set of kernel constraints that can represent both asynchronous and synchronous relations. It was originally developed as part of the UML Profile for MARTE to express causal and temporal constraints of Real-time and Embedded Systems. In this paper, we explore the use of CCSL for modeling scheduling requirements and to conduct schedulability analysis. For this purpose, a dedicated scheduling library of CCSL has been built. This library is endowed with a state-based operational semantics, and is applied to solve issues related to schedulability analysis and latency-insensitive design. We establish schedulability categories and latency-insensitiveness property in the context of the semantics, and solve those issues by using model checking techniques.

Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Close interactions between the cyber and physical worlds occur in time and space frequently. Therefore, both temporal and spatial information should be taken into consideration when specifying properties of CPS systems for verification. However, how to formulate properties specifying spatial together with temporal features is still an unsolved problem in the CPS. In this paper, we propose an approach to analyze the spatio-temproal properties of CPS. A spatio-temporal logic is developed, including the syntax and semantics of the logic. With that logic, properties of both states, transitions and global systems could be specified, paving the way for further verification. To show the efficiency of the approach, a Train Control System is introduced as a case study. Meanwhile, more details about how to specifying properties of CPS systems with our method are elaborated.

In component-based architecture, a component is a unit of computation or a data store. Connectors are architectural building blocks used to model interactions among components. However, in some particular complex real-time systems, it is non-determinate and confused to distinguish some modules functioning as components as well as connectors. Therefore, a unified model method is demanded to describe those modules. In this paper, we propose a method to divide components into reactive and active component based on providing or requiring services when they interact with each other. A reactive component provides services and could call services of other reactive components. Active components call reactive components and are used to coordinate reactive components. Active and reactive timed automata are unified defined by extending timed automata to denote them. Then, we redefine the component composition language and present the semantics of composition of timed automata. A case study of Train Integrity Detection System illustrates the usage of our unified models for active and reactive components.

Switched fuzzy systems can be used to describe the hybrid systems with fuzziness. However, the languages to describe the switching logic and the fuzzy subsystems are, in general, different, and this difference makes the system analysis and implementation hard. In this paper, we use differential Petri net (DPN) as a unified model to represent both the discrete logic and fuzzy dynamic processes. To exam the rationality of the representation, we prove the correctness of the representation for the discrete part and estimate the approximation accuracy of the representation for the dynamic part. Our work provides a way to analyze the switched fuzzy systems by checking the PN and to use the PN model for further system implementation. We demonstrate the benefits of our work via a case study.

Web service composition is a distributed model to construct new web service on top of existing primitive or other composite web services. However, current service technologies, including proposed composition languages, do not address the reliability of web service composition. Thus, it is hard to predict the system reliability. In this paper, we propose a method to compute system reliability based on Service Component Architecture (SCA), a standard that provides a language-independent way to define and compose service components in the system. We first present a formal service component signature model with respect to the specification of the SCA assembly model, and then propose a language-independent dynamic behavior model for specifying the interface behavior of the service component by port activities. Then, the failure behaviors of ports are defined through the Nonhomogeneous Poisson Process (NHPP). Based on the semantics of ports, several rules have been generated to compute reliability of port expressions, thus the overall system reliability can be automatically computed. An Online Shop example from IBM web site is given to illustrate our method, together with a testing bed to calculate port reliability.

We have seen growing interest in validation of a business process model before it is implemented due to the complexity to model business process. In this paper, we propose a method for analyzing and validating the functional correctness of a business process model. Based on our previous work, we model a business process in UML activity diagrams with OCL constraints, then we give a formal semantics of the business process model, finally we validate the model by prototyping. We have developed a tool - AutoPA to support our method. When applying the tool, a business process model specified by UML activity diagrams with OCL constraints is transformed into an executable prototype in Java. Both the control flow dimension and the dataflow dimension of the model are considered. With the prototype, users can validate the functional properties of the business process model in an interactive way. We use a real-world example as a case study: the business process of the first delivery of mortgage archive in a risk mitigation system of a bank.

In this paper, a new method is proposed to measure the performance of service composition. Service composition described with Business Process Execution Language (BPEL) is modeled by a group of fuzzy differential equations, where each equation describes the state change of the service composition. Each service state is measured by a time-dependent fuzzy number that indicates the extent to which the state can be reached in execution. This information of measure can help us to conduct performance analysis, such as estimating response time, throughput, efficiency, and maximum load. This method has the following advantages: 1) It can handle fuzziness such as nondeterministic response time; 2) it treats the system as a box and displays a global picture of execution states to the users so that users know exactly where to improve the performance; 3) it can entirely avoid the state explosion problem, which may be hit by the existing performance analysis methods. A case study demonstrates the advantages of our method.

Assuring the consistency between collaborative services is a challenge problem in service oriented architecture. In this paper, we propose an approach to verifying the consistency of collaborative services based upon model checking. We first introduce an Extended UML Sequence Diagram for modeling dynamic behavior of collaborative service combining with UML State Chart Diagram. And then we define Collaboration-Contracts and obtain the verification model from the dynamic behavior models. Finally, wean automatically verify the consistency of collaborative services in behavior models by using an integrated SPIN-binding modeling tool Trustable MDA we developed to, In addition, a user-friendly service simulator is provided to locate the position of inconsistency.

In this paper, we present a method to measure the survivability of an object-oriented software in design phase. Each component is responsible for this measuring and the relations between components are based on the communication type. Each component can be characterized by a composite Petri net which combines the features of statechart and object diagram. A fuzzy number is introduced to this net to represent uncertain elements that might affect the survivability. Survival possibility theory has been used to produce survivability measure function for each component. A survivability measure index is defined for the system, and we proved that this index is monotonic.

Test data generation is one of the important tasks during software testing. This paper proposes an approach to generating test cases automatically for the unit test of C programs with derived types including pointers, structures and arrays. Our approach combines symbolic execution and concrete execution. The approach captures operations on variables precisely by concrete execution, and thus it is capable of handling derived types. Benefited from symbolic execution, accessing variables as array index can be solved by a substitution strategy. The substitution strategy also translates a path constraint involving variables of derived type to the one containing only primitive variables. An implementation of this approach is integrated into our test case generation tool called CAUT. Experimental results show that our approach is effective to generate test data for derived types.

Based on Continuous Petri Net, we build differential equation model for concurrent programs. The program behavior can be analyzed from the curves of the solutions of the differential equations. We show that a program state can be measured with a number between 0 and 1, called state measure, indicating how much the state can be reached while the program is in execution. Thus, instead of displaying one state at one time, a program can display all states at one time with state measure attached to each state. This information can help us to estimate where and how much the resources have been used. The advantage of our method is that we can avoid state explosion problem while doing program analysis. Our equations can be solved by Matlab and simulated with a tool: Snoopy.