With the widespread application of Large Language Models (LLMs) in the field of natural language processing and software engineering, security vulnerabilities have emerged as a critical concern. Among these, jailbreak attacks represent a prevalent security threat, as they bypass the internal security checks of the model through carefully designed input perturbations, generating malicious outputs which severely may compromise the reliability and security of the LLM-based software tools. Existing defense methods based on reinforcement learning and fine-tuning often suffer from limited generalization, low interpretability, and high computational overhead. To address these limitations, we propose MaskedDefender, a novel defense approach that detects potential attack features by analyzing model's response differences to various inputs. Guided by the principle of key information protection and selective compression, MaskedDefender identifies critical tokens associated with jailbreak attacks by optimizing the gradient of a multi-objective loss function. It then applies soft guidance to steer the model's attention toward these critical tokens. Our approach highlights jailbreak intentions and reduces the model's confusion in identifying such attacks without modifying model parameters. Experimental results show that MaskedDefender outperforms existing defense methods in enabling the model to detect and resist jailbreak attacks, while maintaining both efficiency and effectiveness.

A Dockerfile defines a set of instructions to build Docker images, which can then be instantiated to support containerized applications. Recent studies have revealed a considerable amount of quality issues with Dockerfiles. In this article, we propose a novel approach, Dockerfiles Rule mIning and Violation dEtection ( DRIVE ), to mine implicit rules and detect potential violations of such rules in Dockerfiles. DRIVE first parses Dockerfiles and transforms them to an intermediate representation. It then leverages an efficient sequential pattern mining algorithm to extract potential patterns. With heuristic-based reduction and moderate human intervention, potential rules are identified, which can then be utilized to detect potential violations of Dockerfiles. DRIVE identifies 34 semantic rules and 19 syntactic rules including 9 new semantic rules that have not been reported elsewhere. Extensive experiments on real-world Dockerfiles demonstrate the efficacy of our approach.

Automatic test generation can help verify and develop the behavior of mobile applications. Test reuse based on semantic similarities between applications of the same category has been utilized to reduce the manual effort of Graphical User Interface (GUI) testing. However, most of the existing studies fail to solve the semantic problem of event matching, which leads to the failure of test reuse. To overcome this challenge, we propose TRASM (Test Reuse based on Adaptive Semantic Matching), a test reuse approach based on adaptive strategies to find a better event matching across android mobile applications. TRASM first performs GUI events deduplication on the initial test set obtained from test generation, and then employs an adaptive strategy to find better event matching, which enables reusing the existing test. Preliminary experiments with comparison to baseline methods on 15 applications demonstrate that TRASM can improve the precision of GUI event matching while reducing the failure of test reuse and the running time required for test reuse.

Source code summarization aims to generate concise descriptions for code snippets in a natural language, thereby facilitates program comprehension and software maintenance. In this paper, we propose a novel approach– GSCS –to automatically generate summaries for Java methods, which leverages both semantic and structural information of the code snippets. To this end, GSCS utilizes Graph Attention Networks to process the tokenized abstract syntax tree of the program, which employ a multi-head attention mechanism to learn node features in diverse representation sub-spaces, and aggregate features by assigning different weights to its neighbor nodes. GSCS further harnesses an additional RNN-based sequence model to obtain the semantic features and optimizes the structure by combining its output with a transformed embedding layer. We evaluate our approach on two widely-adopted Java datasets; the experiment results confirm that GSCS outperforms the state-of-the-art baselines.

Deep neural networks (DNNs) have shown remarkable performance in a variety of domains such as computer vision, speech recognition, and natural language processing. Recently they also have been applied to various software engineering tasks, typically involving processing source code. DNNs are well-known to be vulnerable to adversarial examples, i.e., fabricated inputs that could lead to various misbehaviors of the DNN model while being perceived as benign by humans. In this paper, we focus on the code comment generation task in software engineering and study the robustness issue of the DNNs when they are applied to this task. We propose ACCENT (Adversarial Code Comment gENeraTor) , an identifier substitution approach to craft adversarial code snippets, which are syntactically correct and semantically close to the original code snippet, but may mislead the DNNs to produce completely irrelevant code comments. In order to improve the robustness, ACCENT also incorporates a novel training method, which can be applied to existing code comment generation models. We conduct comprehensive experiments to evaluate our approach by attacking the mainstream encoder-decoder architectures on two large-scale publicly available datasets. The results show that ACCENT efficiently produces stable attacks with functionality-preserving adversarial examples, and the generated examples have better transferability compared with the baselines. We also confirm, via experiments, the effectiveness in improving model robustness with our training method.

Code summarization aims to automatically generate functionality descriptions of code snippets. Faithful metrics are needed to measure to which degree the machine generated summaries capture the semantics of the code snippets. Most commonly used metrics in code summarization, such as BLEU -4, METEOR, and ROUGE-L, originate from machine translation and text summarization, and have constantly been found to be inconsistent with human assessment. In this paper, we propose a novel evaluation metric, Consensus-based Code Summarization Evaluation (CCSE), which assigns different semantic weights to the n-grams of the summary. We also provide an algorithm to match the n-gram pairs from the reference and candidate based on the similarities. To validate the effectiveness of our proposed metric, we collect summary pairs from two public Java datasets and calculate the correlation coefficients between CCSE and the human evaluations. The experiment results show that, compared with BLEU-4, METEOR, and ROUGE-L, CCSE is more consistent with the scores assessed by human developers.

With the development of deep neural networks (DNNs) and the publicly available source code repositories, deep code comment generation models have demonstrated reasonable performance on test datasets. However, it has been confirmed in computer vision (CV) and natural language processing (NLP) that DNNs are vulnerable to adversarial examples. In this paper, we investigate how to maintain the performance of the models against these perturbed samples. We propose a simple, but effective, method to improve the robustness by training the model via data augmentation. We conduct experiments to evaluate our approach on two mainstream sequence-sequence (seq2seq) architectures which are based on the LSTM and the Transformer with a large-scale publicly available dataset. The experimental results demonstrate that our method can efficiently improve the capability of different models to defend the perturbed samples.

In service composition, quality‐of‐service (QoS) represents a crucial indicator for the policy adoption. Existing composition strategies rarely address the influence of the environment, which may influence QoS and thus lead to sub‐optimal composition policies in a dynamic environment. In this study, a model‐based service composition approach is proposed. Given the user request, it is possible to first find a set of matching abstract web services (AWSs), and then pull relevant concrete web services (CWSs) based on the AWSs. The set of CWSs can be modelled as a Markov decision process (MDP). In addition, the authors model the environment as a fully probabilistic system, capturing changes of environment probabilistically. The environment model can be further composed of the MDP from the service models, obtaining a monolithic MDP. They demonstrate how the probabilistic verification techniques can be used to find the optimal service selection strategy against their QoS and the environment change. A distinguishing feature of their approach is that the QoS, as well as the dynamic of environment change, is made parametric so that the formal analysis is adaptive to the environment which is of paramount importance for autonomous and self‐adaptive systems. Examples and experiments confirm the feasibility of their approach.

Finger texture (FT) images acquired from different spectral lighting sensors reveal various features. This inspires the idea of establishing a recognition model between FT features collected using two different spectral lighting forms to provide high recognition performance. This can be implemented by establishing an efficient feature extraction and effective classifier, which can be applied to different FT patterns. So, an effective feature extraction method called the surrounded patterns code (SPC) is adopted. This method can collect the surrounded patterns around the main FT features. It is believed that these patterns are robust and valuable. Furthermore, a novel classifier termed the re‐enforced probabilistic neural network (RPNN) is proposed. It enhances the capability of the standard PNN and provides better recognition performance. Two types of FT images from the multi‐spectral Chinese Academy of Sciences Institute of Automation (CASIA) database were employed as two types of spectral sensors were used in the acquiring device: the white (WHT) light and spectral 460 nm of blue (BLU) light. Supporting comparisons were performed, analysed and discussed. The best results were recorded for the SPC by enhancing the equal error rates at 4% for spectral BLU and 2% for spectral WHT. These percentages have been reduced to 0% after utilising the RPNN.

We investigate the complexity of computing entropy of various Markovian models including Markov Chains (MCs), Interval Markov Chains (IMCs) and Markov Decision Processes (MDPs). We consider both entropy and entropy rate for general MCs, and study two algorithmic questions, i.e., entropy approximation problem and entropy threshold problem. The former asks for an approximation of the entropy/entropy rate within a given precision, whereas the latter aims to decide whether they exceed a given threshold. We give polynomial-time algorithms for the approximation problem, and show the threshold problem is in P^CH_3 (hence in PSPACE) and in P assuming some number-theoretic conjectures. Furthermore, we study both questions for IMCs and MDPs where we aim to maximise the entropy/entropy rate among an infinite family of MCs associated with the given model. We give various conditional decidability results for the threshold problem, and show the approximation problem is solvable in polynomial-time via convex programming.

We present a framework for modelling ad-hoc Wireless Sensor Networks (WSNs) and studying both their connectivity properties and their performances in terms of energy consumption, throughput and other relevant indices. Our framework is based on a probabilistic process calculus where system executions are driven by Markovian probabilistic schedulers, allowing us to translate process terms into discrete time Markov chains (DTMCs) and use the probabilistic model checker PRISM to automatically evaluate/estimate the connectivity properties and the energy costs of the networks. To the best of our knowledge, this is the first work that proposes a unique framework for studying qualitative (e.g., by proving the equivalence of components or the correctness of a behaviour) and quantitative aspects of WSNs using a tool that allows both exact and approximate (via Monte Carlo simulation) analyses. We demonstrate our framework at work by considering different communication strategies based on gossip routing protocols, for a typical topology and a mobility scenario.

Markov decision processes (MDPs) are often used for modelling distributed systems with probabilistic failure or randomisation. We consider the problem of model repair for MDPs defined as follows: if the MDP fails to satisfy a property, we aim to find new values for the transition probabilities so that the property is guaranteed to hold, while at the same time the cost of repair is minimised. Because solving the MDP repair problem exactly is infeasible, in this paper we focus on approximate solution methods. We first formulate a region-based approach, which yields an interval in which the minimal repair cost is contained. As an alternative, we also consider sampling based approaches, which are faster but unable to provide lower bounds on the repair cost. We have integrated both methods into the probabilistic model checker PRISM and demonstrated their usefulness in practice using a computer virus case study.

We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.

This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity of bounded reachability properties. This algorithm is based on discretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.

This paper focuses on probabilistic timed automata (PTA), an extension of timed automata with discrete probabilistic branchings. As the regions of these automata often lead to an exponential blowup, reduction techniques are of utmost importance. In this paper, we investigate probabilistic time-abstracting bisimulation (PTaB), an equivalence notion that abstracts from exact time delays. PTaB is proven to preserve probabilistic computational tree logic (PCTL). The region equivalence is a (very refined) PTaB. Furthermore, we provide a non-trivial adaptation of the traditional partition-refinement algorithm to compute the quotient under PTaB. This algorithm is symbolic in the sense that equivalence classes are represented as polyhedra.

The requirement for modifying system structure during system execution is specified by dynamic software architectures. The system architecture style should remain one style or transform within a scope so that some constraints need to be imposed on during the system execution. Our work expands such an idea along two directions in the setting of formalism. The first direction is to model the system by a graph-based calculus stressing the structure. The other direction lies in that we tailor spatial logic to be a suitable logic as the system specification for structure. The model and specification are basis for the model checking algorithm that is to verify whether the system evolution satisfies some structure constraints. We invite a master-slave architecture style as a running example from the beginning and throughout the paper to demonstrate our approach. Such work can be seen as the basis of the structure analysis for architectures.

The open and dynamic Internet environment greatly urges software entities that are distributed on different locations to coordinate with each other to accomplish a computing task. Software architecture is applied to abstract the software entities to be components and the coordination between them to be connectors and then a model is extracted as the architecture on which the design, analysis and verification are based. Currently, the notion of dynamic software architectures that can modify their architecture and enact modifications during the system execution has become one of the most active research areas. In this paper, we focus on the dynamic evolution of system structure other than coordination mechanisms (e.g. communication protocols). It is widely recognized that some restrictions should be imposed on the system evolution to ensure that the system structure may remain one style or transform within a scope. These conditions, to a large extent, make the system execute under control as expected.

The /spl pi/-calculus is one of the most important mobile process calculi and has been well studied in literature. Temporal logic is thought of as a good compromise between description convenience and abstraction and can support useful computational applications, such as model-checking. We use a symbolic transition graph inherited from /spl pi/-calculus to model concurrent systems. A wide class of processes, that is, finite-control processes, can be represented as a finite symbolic transition graph. A new version of modal logic for the /spl pi/-calculus, an extension of the modal /spl mu/-calculus with Boolean expressions over names, and primitives for name input and output are introduced as an appropriate temporal logic for the /spl pi/-calculus. Since we make a distinction between proposition and predicate, the possible interactions between recursion and first-order quantification can be solved. A concise semantics interpretation for our modal logic is given. Based on this work, we provide a model checking algorithm for the logic. This algorithm follows Winskel's well known tag set method to deal with the fixpoint operator. As for the problem of name instantiating, our algorithm follows the 'on-the-fly' style, and systematically employs schematic names. The correctness of the algorithm is shown.