Metric interval temporal logic specification elicitation and debugging

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

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

11 Citations (Scopus)

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

Fingerprint

Temporal logic
Specifications
Testing
Graphical user interfaces
Real time systems
Embedded systems
Redundancy
Formal specification
Engineers
Networks (circuits)

Keywords

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

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

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

Metric interval temporal logic specification elicitation and debugging. / Dokhanchi, Adel; Hoxha, Bardh; Fainekos, Georgios.

2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc., 2015. p. 70-79 7340472.

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

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., 7340472, Institute of Electrical and Electronics Engineers Inc., pp. 70-79, ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, United States, 9/21/15. https://doi.org/10.1109/MEMCOD.2015.7340472
Dokhanchi A, Hoxha B, Fainekos G. Metric interval temporal logic specification elicitation and debugging. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc. 2015. p. 70-79. 7340472 https://doi.org/10.1109/MEMCOD.2015.7340472
Dokhanchi, Adel ; Hoxha, Bardh ; Fainekos, Georgios. / Metric interval temporal logic specification elicitation and debugging. 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc., 2015. pp. 70-79
@inproceedings{ea029cae401f430c9fa4b9b3811605d4,
title = "Metric interval temporal logic specification elicitation and debugging",
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.",
keywords = "Debugging, Natural languages, Real-time systems, Testing, Timing, Visualization",
author = "Adel Dokhanchi and Bardh Hoxha and Georgios Fainekos",
year = "2015",
month = "11",
day = "30",
doi = "10.1109/MEMCOD.2015.7340472",
language = "English (US)",
isbn = "9781509002375",
pages = "70--79",
booktitle = "2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Metric interval temporal logic specification elicitation and debugging

AU - Dokhanchi, Adel

AU - Hoxha, Bardh

AU - Fainekos, Georgios

PY - 2015/11/30

Y1 - 2015/11/30

N2 - 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.

AB - 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.

KW - Debugging

KW - Natural languages

KW - Real-time systems

KW - Testing

KW - Timing

KW - Visualization

UR - http://www.scopus.com/inward/record.url?scp=84960969480&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84960969480&partnerID=8YFLogxK

U2 - 10.1109/MEMCOD.2015.7340472

DO - 10.1109/MEMCOD.2015.7340472

M3 - Conference contribution

AN - SCOPUS:84960969480

SN - 9781509002375

SP - 70

EP - 79

BT - 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015

PB - Institute of Electrical and Electronics Engineers Inc.

ER -