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

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Contribution to journalArticle

4 Scopus citations

Abstract

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
Volume17
Issue number2
DOIs
StatePublished - Dec 1 2017

Keywords

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

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint 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