Formal requirement debugging for testing and verification of cyber-physical systems

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Contribution to journalArticlepeer-review

14 Scopus citations


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.

Original languageEnglish (US)
Article number34
JournalACM Transactions on Embedded Computing Systems
Issue number2
StatePublished - Dec 2017


  • CPS
  • LTL
  • MITL
  • SAT
  • SMT
  • STL

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture


Dive into the research topics of 'Formal requirement debugging for testing and verification of cyber-physical systems'. Together they form a unique fingerprint.

Cite this