In general, system testing and verification should be conducted with respect to formal specifications. However, the development of formal specifications is a challenging and error prone task, even for experts. This is especially true when considering complex spatio-temporal requirements in real-time embedded systems, mixed-signal circuits, or more generally, software-controlled physical systems. In this work, we present a framework for the elicitation and debugging of formal specifications. The elicitation of formal specifications is handled through a graphical user interface. The debugging algorithm checks inconsistent and wrong specifications. Namely, it detects validity, redundancy and vacuity issues in formal specifications developed in a fragment of Metric Interval Temporal Logic (MITL). The algorithm informs system engineers on any issues in their specifications. This improves the specification elicitation process and, ultimately, the testing and verification process. Finally, we present experimental results on specifications that typically appear in Cyber Physical Systems (CPS) applications. Application of our specification debugging tool on user derived requirements shows that the aforementioned issues are common. Therefore, the algorithm can help developers to correct their specifications and avoid wasted effort on checking incorrect requirements.
|Title of host publication
|2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
|Institute of Electrical and Electronics Engineers Inc.
|Number of pages
|Published - Nov 30 2015
|ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 - Austin, United States
Duration: Sep 21 2015 → Sep 23 2015
|ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
|9/21/15 → 9/23/15
- Natural languages
- Real-time systems
ASJC Scopus subject areas
- Hardware and Architecture