[en] 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.
Centre de recherche :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation
Disciplines :
Sciences informatiques
Auteur, co-auteur :
MENGHI, Claudio ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
VIGANO, Enrico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
BIANCULLI, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
BRIAND, Lionel ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
Co-auteurs externes :
no
Langue du document :
Anglais
Titre :
ThEodorE: a Trace Checker for CPS Properties
Date de publication/diffusion :
mai 2021
Nom de la manifestation :
International Conference on Software Engineering (ICSE 2021)
Date de la manifestation :
from 23-05-2021 to 29-05-2021
Titre de l'ouvrage principal :
Companion Proceedings of the 43rd International Conference on Software Engineering
Maison d'édition :
IEEE
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
Projet européen :
H2020 - 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
C. Menghi, E. Viganò, D. Bianculli, and L. C. Briand, "Theodore-trace-checker, " Feb. 2021. [Online]. Available: https: //doi. org/10. 5281/zenodo. 4506795
C. Menghi, E. Viganò, D. Bianculli, and L. C. Briand, "Trace-checking CPS properties: Bridging the cyberphysical gap, " in International Conference on Software Engineering (ICSE). ACM, 2021.