Metric interval temporal logic specification elicitation and debugging

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages70-79
Number of pages10
ISBN (Print)9781509002375
DOIs
StatePublished - Nov 30 2015
EventACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 - Austin, United States
Duration: Sep 21 2015Sep 23 2015

Other

OtherACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
CountryUnited States
CityAustin
Period9/21/159/23/15

Keywords

  • Debugging
  • Natural languages
  • Real-time systems
  • Testing
  • Timing
  • Visualization

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Metric interval temporal logic specification elicitation and debugging'. Together they form a unique fingerprint.

  • Cite this

    Dokhanchi, A., Hoxha, B., & Fainekos, G. (2015). Metric interval temporal logic specification elicitation and debugging. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 (pp. 70-79). [7340472] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/MEMCOD.2015.7340472