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.

Most researchers have tried to enhance the robustness of deep neural networks (DNNs) by revealing and repairing the vulnerability of DNNs with specialized adversarial examples. Parts of the attack examples have imperceptible perturbations restricted by Lp norm. However, due to their high-frequency property, the adversarial examples can be defended by denoising methods and are hard to realize in the physical world. To avoid the defects, some works have proposed unrestricted attacks to gain better robustness and practicality. It is disappointing that these examples usually look unnatural and can alert the guards. In this paper, we propose Adversarial Lightness Attack (ALA), a white-box unrestricted adversarial attack that focuses on modifying the lightness of the images. The shape and color of the samples, which are crucial to human perception, are barely influenced. To obtain adversarial examples with a high attack success rate, we propose unconstrained enhancement in terms of the light and shade relationship in images. To enhance the naturalness of images, we craft the naturalness-aware regularization according to the range and distribution of light. The effectiveness of ALA is verified on two popular datasets for different tasks (i.e., ImageNet for image classification and Places-365 for scene recognition).

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.

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.