Leveraging Natural Language Processing for a Consistency Checking Toolchain of Automotive Requirements
Vincent Bertram, Hendrik Kausch, Evgeny Kusmenko, Haron Nqiri, Bernhard Rumpe⋆, Constantin Venhoff
Abstract
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.