In the automotive industry, specifications often consist of a large number of textual requirements. These requirements are linguistically ambiguous and written in informal language. Utilizing Structured English for requirements eliminates ambiguity, improves data quality, and supports further automated processing while maintaining readability. The recent development of large language models enables a fully automated translation approach using few-shot learning. To deal with the limited context size of large language models, an improved algorithm, OptKATE, is presented to find an ideal set of requirements for few-shot learning. Structured English can be used as a basis for further formalization. This capability is key in creating an interface between natural language processing and verification, in our case, consistency analysis using the Z3 SMT solver. We implemented a grammar for translating Structured English into TCTL using the MontiCore workbench. Furthermore, since SMT-based methods currently rely on manual precondition satisfaction and do not tackle conflicting preconditions automatically, we propose a scenario generation algorithm that generates potential scenarios using the specification and checks the requirements against them. Through this approach, we can better identify and resolve conflicting preconditions, ultimately improving the consistency of requirements. Our toolchain is evaluated using an automotive requirements dataset provided by former Daimler AG.

Systems engineering, in particular in the automotive domain, needs to cope with the massively increasing numbers of requirements that arise during the development process. The language in which requirements are written is mostly informal and highly individual. This hinders automated processing of requirements as well as the linking of requirements to models. Introducing formal requirement notations in existing projects leads to the challenge of translating masses of requirements and the necessity of training for requirements engineers. In this paper, we derive domain-specific language constructs helping us to avoid ambiguities in requirements and increase the level of formality. The main contribution is the adoption and evaluation of few-shot learning with large pretrained language models for the automated translation of informal requirements to structured languages such as a requirement DSL.

Component and Connector (C&C) view specifications, with corresponding verification and synthesis techniques, have been recently suggested as a means for formal yet intuitive structural specification of C&C models. In this paper we report on our recent experience in applying C&C views in industrial practice, where we aimed to answer questions such as: could C&C views be practically used in industry, what are challenges of systems engineers that the use of C&C views could address, and what are some of the technical obstacles in bringing C&C views to the hands of systems engineers. We describe our experience in detail and discuss a list of lessons we have learned, including, e.g., a missing abstraction concept in C&C models and C&C views that we have identified and added to the views language and tool, that engineers can create graphical C&C views quite easily, and how verification algorithms scale on real-size industry models. Furthermore, we report on the non-negligible technical effort needed to translate Simulink block diagrams to C&C models. We make all materials mentioned and used in our experience electronically available for inspection and further research.