Formal Requirement Elicitation and Debugging for Testing and Verification of Cyber-Physical Systems
This addresses the challenge of ensuring correct specifications for Cyber-Physical Systems, which is crucial for testing and verification, though it appears incremental as it builds on existing debugging methods.
The paper tackles the problem of formal specification errors in Cyber-Physical Systems by presenting a framework for elicitation and debugging, including two algorithms for checking temporal logic and reactive requirements, and shows through a user study that the framework can resolve many common errors.
A framework for the elicitation and debugging of formal specifications for Cyber-Physical Systems is presented. The elicitation of specifications is handled through a graphical interface. Two debugging algorithms are presented. The first checks for erroneous or incomplete temporal logic specifications without considering the system. The second can be utilized for the analysis of reactive requirements with respect to system test traces. The specification debugging framework is applied on a number of formal specifications collected through a user study. The user study establishes that requirement errors are common and that the debugging framework can resolve many insidious specification errors.