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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Streamlined, Formal Approach to Requirements-Based Testing

  • Andreas Katis,
  • Anastasia Mavridou,
  • Tom Pressburger

摘要

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.