In recent years, Text-to-Image (T2I) models have garnered significant attention due to their remarkable advancements. However, security concerns have emerged due to their potential to generate inappropriate or Not-Safe-For-Work (NSFW) images. In this paper, inspired by the observation that texts with different semantics can lead to similar human perceptions, we propose an LLM-driven perception-guided jailbreak method, termed PGJ. It is a black-box jailbreak method that requires no specific T2I model (model-free) and generates highly natural attack prompts. Specifically, we propose identifying a safe phrase that is similar in human perception yet inconsistent in text semantics with the target unsafe word and using it as a substitution. The experiments conducted on six open-source models and commercial online services with thousands of prompts have verified the effectiveness of PGJ.

The advent of local continuous image function (LIIF) has garnered significant attention for arbitrary-scale super-resolution (SR) techniques. However, while the vulnerabilities of fixed-scale SR have been assessed, the robustness of continuous representation-based arbitrary-scale SR against adversarial attacks remains an area warranting further exploration. The elaborately designed adversarial attacks for fixed-scale SR are scale-dependent, which will cause time-consuming and memory-consuming problems when applied to arbitrary-scale SR. To address this concern, we propose a simple yet effective “scale-invariant” SR adversarial attack method with good transferability, termed SIAGT. Specifically, we propose to construct resource-saving attacks by exploiting finite discrete points of continuous representation. In addition, we formulate a coordinate-dependent loss to enhance the cross-model transferability of the attack. The attack can significantly deteriorate the SR images while introducing imperceptible distortion to the targeted low-resolution (LR) images. Experiments carried out on three popular LIIF-based SR approaches and four classical SR datasets show remarkable attack performance and transferability of SIAGT.

Formalization of intended requirements is indispensable when using formal methods in software development. However, translating Natural Language (NL) requirements into formal specifications, such as Linear Temporal Logic (LTL), is error-prone. Although Large Language Models (LLMs) offer the potential for automatically translating unstructured NL requirements to LTL formulas, general-purpose LLMs face two major problems: First, low accuracy in translation. Second, high cost of model training and tuning. To tackle these challenges, we propose a new approach that combines dynamic prompt generation with human-computer interaction to leverage LLM for an accurate and efficient translation of unstructured NL requirements to LTL formulas. Our approach consists of two techniques: 1) Dynamic Prompt Generation, which automatically generates the most appropriate prompts for translating the inquired NL requirements. 2) Interactive Prompt Evolution, which helps LLMs to learn from previous translation errors, i.e., erroneous formalizations are amended by users and added as new prompt fragments. Our approach achieves remarkable performance in publicly available datasets from two distinct domains, comprising 36 and 255,000 NL-LTL pairs, respectively. Without human interaction, our method achieves up to 94.4% accuracy. When our approach is extended to another domain, the accuracy improves from an initial 27% to 78% under interactive prompt evolution.

Interlocking has long played a crucial role in railway systems. Its functional correctness, particularly concerning safety, forms the foundation of the entire signaling system. To date, numerous efforts have been made to formally model and verify interlocking systems. However, two main problems persist in most prior work: (1) The formal description of the interlocking system heavily depends on reusing existing models, which often results in overgeneralization and failing to fully utilize the intrinsic characteristics of interlocking systems. (2) The verification techniques of current approaches may quickly become outdated, and there is no adaptable method to integrate state-of-the-art verification algorithms or tools.

The emerging Internet of Things (IoT) applications, such as intelligent transportation based on vehicular-lane accurate positioning, have a growing demand for precise and reliable positioning with global navigation satellite systems (GNSSs). It is desirable to use GNSS modules in smartphones to achieve high-precision positioning. The GNSS modules in some brands of smartphones thus far are able to track the new L5 signals of GPS and QZSS, E5a signals of Galileo, and B2a signals of BeiDou-3. The L5/E5a/B2a signals have higher quality due to their signal structure, which provides an important potential for high-precision positioning in smartphones. In this article, we will study the quality of L5/E5a/B2a signals, and their superiorities in integer ambiguity resolution (IAR) and precise positioning with respect to the L1/E1/B1 signals from GPS, QZSS, Galileo, and Beidou-2/3 satellites. The signal quality is evaluated in terms of observation precision, multipath, double-differenced ambiguity fractions, and ambiguity dilution of precision (ADOP). In addition, we propose a new weighting model that takes into account the variation range of carrier-to-noise density ratio ($C / N $textsubscript 0). The results indicate that the Beidou-3 B2a signal has comparable quality to L5/E5a signals of other systems, and all of them are better than the L1/E1/B1 signals. However, the ambiguity fractions of B2a signals diverge abruptly in some periods, resulting in the unsuccessful ambiguity fixing. The L5/E5a/B2a signals can generally obtain higher IAR fix-rate and positioning accuracies than the L1/E1/B1 signals. The new weighting model can capture the smartphone noise characteristics better than the traditional weighting model, thus improving the positioning accuracy.

The rapid development of machine learning (ML) systems has raised many concerns over their quality.Due to the inherent complexity and uncertainty, most of the traditional quality assurance techniques have been challenged, including requirements specification.Current strategies mainly focus on model extraction from existing neural networks to improve interpretability and facilitate system analysis, but failing to include user expectations on the system.To handle the problem, this paper proposes a specification framework for ML requirements where each ML system is regarded as a set of snapshot systems along the evolvement process.There are 3 layers in the framework and the hierarchy indicates that higher-level models need to be built based on lower-level ones.The bottom layer consists of meta snapshot model and meta data model serving as the meta models for snapshot systems and data requirements respectively.The middle layer is for snapshot models each describing a snapshot system through relations between its outputs produced with different inputs.The top layer is a learning model capturing the evolvement process by transitions among snapshot models.These transitions are activated by data models instantiated from meta data model.We adopt the specification of a self-driving system to illustrate the framework.

High-level representation-guided pixel denoising and adversarial training are independent solutions to enhance the robustness of CNNs against adversarial attacks by pre-processing input data and re-training models, respectively. Most recently, adversarial training techniques have been widely studied and improved while the pixel denoising-based method is getting less attractive. However, it is still questionable whether there exists a more advanced pixel denoising-based method and whether the combination of the two solutions benefits each other. To this end, we first comprehensively investigate two kinds of pixel denoising methods for adversarial robustness enhancement (i.e., existing additive-based and unexplored filtering-based methods) under the loss functions of image-level and semantic-level, respectively, showing that pixel-wise filtering can obtain much higher image quality (e.g., higher PSNR) as well as higher robustness (e.g., higher accuracy on adversarial examples) than existing pixel-wise additive-based method. However, we also observe that the robustness results of the filtering-based method rely on the perturbation amplitude of adversarial examples used for training. To address this problem, we propose predictive perturbation-aware & pixel-wise filtering, where dual-perturbation filtering and an uncertainty-aware fusion module are designed and employed to automatically perceive the perturbation amplitude during the training and testing process. The method is termed as AdvFilter. Moreover, we combine adversarial pixel denoising methods with three adversarial training-based methods, hinting that considering data and models jointly is able to achieve more robust CNNs. The experiments conduct on NeurIPS-2017DEV, SVHN and CIFAR10 datasets and show advantages over enhancing CNNs' robustness, high generalization to different models and noise levels.

The advance of deep learning makes it possible to empower safety-critical systems with intelligent capabilities.However, its intelligent component, i.e., deep neural network, is difficult to formally verify due to the large scale and intrinsic complexity of the verification problem.Abstraction has been proved to be an effective way of improving the scalability.A challenging problem in abstraction is that it is difficult to achieve a balance between the size reduced and output overestimation caused by abstraction.In this work, we propose an effective fine-grained approach to abstract neural networks.Our approach is fine-grained in that we identify four cases that should be abstracted independently under a certain neuron prioritization strategy.This allows us to merge more neurons in networks and meanwhile maintain a relatively low output overestimation.Experimental results show that our approach outperforms other existing abstraction approaches by significantly reducing the scale of target deep neural networks with small overestimation.

Software Product Line deals with the development of product families for diverse market needs and includes feature model to describe the structure of the included products. Since feature model is lack of detailed specification of individual features, some behavior-oriented methods have been proposed to analyze the inner functionalities of features. But how these functions relate to the feature model remains a problem and a systematic approach is still needed to support the whole process of product family modeling. This paper provides a formal engineering approach to modeling product family where feature model evolves as individual features are formalized through informal, semi-formal and formal stages. For each stage, a set of evolvement rules are given to guide the refactoring of the feature model which will then serve as a basis for formal specifications of individual features. Such an iterative process repeats until achieving a feature model with consistent feature specifications. A case study is described to illustrate the effectiveness of our approach.

Requirements-based testing is one of the most commonly used ways to ensure the correctness of software, especially for embedded control software in safety-critical domains such as spacecraft and railway systems. Many industrial standards such as the DO-333 and EN50128 also request rigorous requirements-based software testing. To test embedded control software effectively and efficiently, generating high-quality test cases automatically is extremely important. However, existing methods for generating test cases from requirements require intensive manual efforts and expertise. To address this problem, we proposed an automatic requirements-based software testing method for embedded control software. To obtain automatic test case generation and precise test oracles derivation, requirements specification should be precise and readable for the industrial practitioners. Therefore, we use the light-weight domain-specific formal description language, CASDL (Casco Accurate Specification Description Language) for the industrial practitioners to define software requirements into formal specifications at the first step. Based on the formal specification, we propose an algorithm to automatically generate test inputs that satisfy the MC/DC criteria suggested by typical industrial standards and precise test oracles can be derived by “running” the specification with such test inputs. To this end, we proposed an algorithm for simulating the formal specification to generate the test oracles, i.e., the expected outputs corresponding to the test inputs. To facilitate the application of this method in the industry, we have built a tool that can automatically perform the overall testing process. To validate and evaluate its effectiveness in real industrial projects, we have applied it in testing a real Automatic Train Protection (ATP) system provided by our industrial partner, the Casco Signal Co., Ltd (one of the largest railway control system companies in China). In the case study on ATP requirements, our approach generated test cases for 129 requirement items following MC/DC criteria and caught 40 inconsistencies between Casco’s requirements and implementation.

At this moment, GAN-based image generation methods are still imperfect, whose upsampling design has limitations in leaving some certain artifact patterns in the synthesized image. Such artifact patterns can be easily exploited (by recent methods) for difference detection of real and GAN-synthesized images. However, the existing detection methods put much emphasis on the artifact patterns, which can become futile if such artifact patterns were reduced.

Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

Formal method is a promising solution for precise software requirements modeling and V&V (Validation and Verification). However, domain experts are suffering from using complex mathematics formal notations to precisely describe their domain specific software requirements. Meanwhile, the lack of systematic engineering methodologies that can effectively encompass precise requirements modeling and rigorous requirements V&V makes the application of formal methods in industry still a big challenge. To tackle this challenge, in this paper, we present a domain experts centric approach to the formal requirements modeling and V&V in the domain of embedded control software. The major advancements of the approach are: 1) a domain-specific and systematic engineering approach to the formal requirements specification construction and 2) scenario-based requirements validation and verification requirements technique. Specifically, the approach offers a domain-specific template for formal specification construction through a three-step specification evolution process. For formal requirements V&V, diagrams are derived from formal specification and domain experts' concerned scenarios can be checked based on the diagrams. These modeling and V&V technologies are coherently incorporated in the approach and fully automated by a supporting tool. We have applied the approach real software projects of our industrial partners. The experimental results show that it significantly facilitates the formal modeling and V&V in industry.

We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet users' expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well inter-related. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https://youtu.be/BX0yv8pRMWs.

Knowledge graphs have been widely adopted, in large part owing to their schema-less nature.It enables knowledge graphs to grow seamlessly and allows for new relationships and entities as needed.Natural language questions are the most intuitive way of formulating an information need.People can formulate questions to express their information needs.Natural language questions as a query language present an ideal compromise between keyword and structured querying.Questions can be used to express complex information needs that cannot be expressed as keywords without a significant loss in structure and semantics.Knowledge graph has abundant natural semantics and can contain various and more complete information.Its expression mechanism is closer to natural language.We propose to clarify the expression of knowledge graph as a whole.We use knowledge graph to solve the Five Ws problems respectively which are guided by interrogative words such as who/when, what, how and why.We also propose to specify knowledge graph in a progressive manner as four basic forms including data graph, information graph, knowledge graph and wisdom graph.

Since Internet of Things (IoT) applications are deployed within open physical environments, their executions suffer from a wide spectrum of uncertain factors (e.g., network delay, sensor inputs). Although ThingML is a promising IoT modeling and specification language which enables the fast development of resource-constrained IoT applications, it lacks the capability to model such uncertainties and quantify their effects. Consequently, within uncertain environments the quality and performance of IoT applications generated from ThingML designs cannot be guaranteed. To explore the overall runtime performance variations caused by environmental uncertainties, this paper proposes a quantitative uncertainty evaluation framework for ThingML-based IoT designs. By adopting network of priced timed automata as the model of computation and statistical model checking as the evaluation engine, our approach can model uncertainties caused by external environments as well as support various kinds of performance queries on the extended ThingML designs. Experimental results of two comprehensive case studies demonstrate the efficacy of our approach.

Although formal specification is considered as a potential technique for improving the accuracy of requirements documentation and the quality of software product, the difficulty of using formal notations leads to the gap between this technique and the practice of software development. Many approaches for solving this problem were proposed. Most of them provide automatic transformation from informal requirements into formal specifications. However, rather than clarifying and formalizing requirements on the semantic level, they only use syntactic rules to translate between different languages. To handle the challenge, this paper describes an approach for formal specification construction based on pattern knowledge. The knowledge is composed of a set of inter-related specification patterns. Each pattern defines the method for formalizing one kind of function, including derivation knowledge for guiding the clarification of the function and transformation knowledge for formally representing the clarified function. A supporting tool is also described in the paper which derives necessary function details of the intended requirement through interactions by applying the derivation knowledge and transforms these details into formal specifications by applying the transformation knowledge. An experiment on the tool is held and the result shows that the tool can help formalize requirements efficiently and enhance the quality of the resultant formal specifications.

Service-based software (SBS) modeling is considered as a promising way to develop high-quality service-based systems. One major challenge of this methodology is how to effectively utilize existing software services in the process of system modeling to ensure the reliability of the system while reducing the development cost. In this paper, we propose an evolutionary method for the formal specification construction of SBS to tackle this problem. Initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected and adopted. Candidate services are discovered through a keyword-based searching. Then the services are analyzed from both the structural and behavioral perspectives for filtering. A specification-based testing technique is exploited to rigorously determine which candidate services are finally selected. The selected services are incorporated into the formal design model of the system. We present a case study that was conducted for evaluating the usability of the method. We have also developed a prototype tool for supporting the method to be applied in practice.

Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations pre^*(C) of a regular set C of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute pre^*(C) for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations post^*(C) of a regular set C of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute pre^*(C) and post^*(C). Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.

Despite the effectiveness of requirements formalization in producing accurate requirements documentation, thistechnique can hardly be accepted by software industry mainlydue to the difficulty in manipulating formal notations by practitioners. To handle the challenge, this paper describes aninteractive tool for supporting requirements formalization basedon specification pattern knowledge comprising a set of inter-relatedspecification patterns. Each pattern defines the knowledge forformalizing one kind of function, including derivation knowledgefor guiding the clarification of the function and transformation knowledge for formally representing the clarified function. The tool derives necessary function details of the intendedrequirement through interactions by applying the derivationknowledge and transforms these details into formal specificationsby applying the transformation knowledge.

WiMax (Worldwide Interoperability for Microwave Access, IEEE 802.16) is a standard-based wireless technology, which uses Privacy Key Management (PKM) protocol to provide authentication and key management. Three versions of PKM protocol have been released and the third version (PKMv3) strengthens the security by enhancing the message management. In this paper, a formal analysis of PKMv3 protocol is presented. Both the subscriber station (SS) and the base station (BS) are modeled as processes in our framework. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK), which are produced by BS. Moreover, the PKMv3 model is constructed through the discrete-time PROMELA (DT-PROMELA) language and the tool DT-Spin implements the PKMv3 model with lifetime. Finally, we simulate communications between SS and BS and some properties are verified, i.e. liveness, succession and message consistency, which are extracted from PKMv3 and specified using Linear Temporal Logic (LTL) formulae and assertions. Our model provides a basis for further verification of PKMv3 protocol with time characteristic.

Service-based software modeling is considered as an effective technique for developing high-quality service-based systems. One major challenge of this approach is how to effectively utilize existing software services in the process of system modeling to ensure the reliability of the system while reducing the development cost and effort. In this paper, we propose a novel formal engineering framework by integrating an evolutionary service selection approach into a formal engineering method to tackle this problem. In the framework, initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected, and employed. Candidate services are discovered through a keyword-based searching. A static behavior analysis technique is then used to filter the candidate services and a specification-based testing method is adopted to rigorously select the candidate services. The selected services are finally incorporated into the formal design model of the system. We present an empirical case study that was conducted for evaluating the usability of our framework by applying it to develop a travel agency system. The result of the study demonstrates several advantages of the framework over existing approaches but meanwhile also shows some limitation in practice.

Currently most web services are published without sufficient functional behavior descriptions, which makes it difficult for developers to accurately select services according to the expected functions of their target systems. In this paper, we propose a formal specification-based testing approach to accurate service selection. Requirements upon candidate services are refined into formal specifications in terms of functional scenarios. Test cases for each service operation are basically generated from its associated functional scenarios. Since the internal variables of stateful services are not allowed to be directly monitored from user-end, state transitions of these internal variables can only be checked through running inter-related operations in combination. In particular, functional scenario pairs are used as the foundation for test sequences generation so that potential combinations of interrelated operations can be tested. Conformance of candidate services with respect to users' requirements is determined based on the analysis of testing results. A running example is illustrated to demonstrate the application of this approach. We have also conducted experiments to evaluate the feasibility and the effectiveness of our conformance testing approach.

Service-oriented computing advocates the development of new software or services on the basis of existing services. This paradigm shows a great potential of achieving high productivity and low cost, but it faces a challenge in efficiently and correctly using existing services in producing a new application and ensuring its reliability. Building a formal model using a formal specification language allows the developer to thoroughly understand what existing services are needed for the new application, but how to construct the model so that it can effectively facilitate the developer to recognize the appropriate services still remains an open problem. In this paper, we describe an approach to applying the SOFL formal engineering method to the modeling of a service-oriented system by means of a case study. In particular, we focus on the issue of how to apply the SOFL three-step modeling approach to the construction of a formal specification for a service-based system, exploring the general principle and specific techniques for reusing existing services in developing a system model.