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

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Contribution to journalArticle

2 Citations (Scopus)

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

Fingerprint

Specifications
Testing
Temporal logic
Cyber Physical System
Formal specification

Keywords

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

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Cite this

Formal requirement debugging for testing and verification of cyber-physical systems. / Dokhanchi, Adel; Hoxha, Bardh; Fainekos, Georgios.

In: ACM Transactions on Embedded Computing Systems, Vol. 17, No. 2, 34, 01.12.2017.

Research output: Contribution to journalArticle

@article{80b0a5867e574402ba294243d3e4d4ae,
title = "Formal requirement debugging for testing and verification of cyber-physical systems",
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.",
keywords = "CPS, LTL, MITL, SAT, SMT, STL",
author = "Adel Dokhanchi and Bardh Hoxha and Georgios Fainekos",
year = "2017",
month = "12",
day = "1",
doi = "10.1145/3147451",
language = "English (US)",
volume = "17",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

TY - JOUR

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

AU - Dokhanchi, Adel

AU - Hoxha, Bardh

AU - Fainekos, Georgios

PY - 2017/12/1

Y1 - 2017/12/1

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

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

KW - CPS

KW - LTL

KW - MITL

KW - SAT

KW - SMT

KW - STL

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

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

U2 - 10.1145/3147451

DO - 10.1145/3147451

M3 - Article

VL - 17

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 2

M1 - 34

ER -