A Streamlined, Formal Approach to Requirements-Based Testing
摘要
Techniques that leverage formalized requirements as input can automate test generation and provide coverage metrics. However, the manual process of formalizing these inputs is often unintuitive and error-prone and cannot be streamlined in an industrial setting. To this end, this paper presents a formal framework that enables the automated generation of tests from requirements written in intuitive structured natural language. Our contributions are twofold: (1) We extend prior work on requirements-based testing to account for both future and past fragments of Linear Temporal Logic (LTL), including bounded operators. Our approach is defined inductively over the extended LTL syntax and is proven sound and complete. (2) We extend two existing NASA tools that support specification of requirements in structured natural language and analysis of Matlab/Simulink models. Our extensions enhance these tools with test case generation capabilities and provide a streamlined approach to testing Matlab/Simulink models. Finally, we validate our framework using real-world case studies from Lockheed Martin and NASA.