ThEodorE: A Trace Checker for CPS Properties

Claudio Menghi, Enrico Vigano, Domenico Bianculli, Lionel C. Briand

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

ThEodorE is a trace checker for Cyber-Physical systems (CPS). It provides users with (i) a GUI editor for writing CPS requirements; (ii) an automatic procedure to check whether the requirements hold on execution traces of a CPS. ThEodorE enables writing requirements using the Hybrid Logic of Signals (HLS), a novel, logic-based specification language to express CPS requirements. The trace checking procedure of ThEodorE reduces the problem of checking if a requirement holds on an execution trace to a satisfiability problem, which can be solved using off-the-shelf Satisfiability Modulo Theories (SMT) solvers. This artifact paper presents the tool support provided by ThEodorE.

Original languageEnglish
Title of host publicationProceedings - 2021 IEEE/ACM 43rd International Conference on Software Engineering
Subtitle of host publicationCompanion Proceedings, ICSE-Companion 2021
PublisherIEEE Computer Society
Pages183-184
Number of pages2
ISBN (Electronic)9781665412193
DOIs
Publication statusPublished - May 2021
Externally publishedYes
Event43rd IEEE/ACM International Conference on Software Engineering: Companion, ICSE-Companion 2021 - Virtual, Online, Spain
Duration: 25 May 202128 May 2021

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Conference

Conference43rd IEEE/ACM International Conference on Software Engineering: Companion, ICSE-Companion 2021
Country/TerritorySpain
CityVirtual, Online
Period25/05/2128/05/21

Keywords

  • Formal methods
  • Languages
  • Monitors
  • Semantics
  • Specification
  • Validation

Fingerprint

Dive into the research topics of 'ThEodorE: A Trace Checker for CPS Properties'. Together they form a unique fingerprint.

Cite this