Paper published in a book (Scientific congresses, symposiums and conference proceedings)
Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
Menghi, Claudio; Vigano, Enrico; Bianculli, Domenico et al.
2021In Proceedings of the 43rd International Conference on Software Engineering (ICSE 2021)
Peer reviewed
 

Files


Full Text
ThEodorE.pdf
Author postprint (270.89 kB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Monitors; Languages; Specification; Validation; Formal methods; Semantics
Abstract :
[en] Cyber-physical systems combine software and physical components. Specification-driven trace-checking tools for CPS usually provide users with a specification language to express the requirements of interest, and an automatic procedure to check whether these requirements hold on the execution traces of a CPS. Although there exist several specification languages for CPS, they are often not sufficiently expressive to allow the specification of complex CPS properties related to the software and the physical components and their interactions. In this paper, we propose (i) the Hybrid Logic of Signals (HLS), a logic-based language that allows the specification of complex CPS requirements, and (ii) ThEodorE, an efficient SMT-based trace-checking procedure. This procedure reduces the problem of checking a CPS requirement over an execution trace, to checking the satisfiability of an SMT formula. We evaluated our contributions by using a representative industrial case study in the satellite domain. We assessed the expressiveness of HLS by considering 212 requirements of our case study. HLS could express all the 212 requirements. We also assessed the applicability of ThEodorE by running the trace-checking procedure for 747 trace-requirement combinations. ThEodorE was able to produce a verdict in 74.5% of the cases. Finally, we compared HLS and ThEodorE with other specification languages and trace-checking tools from the literature. Our results show that, from a practical standpoint, our approach offers a better trade-off between expressiveness and performance.
Research center :
ULHPC - University of Luxembourg: High Performance Computing
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Disciplines :
Computer science
Author, co-author :
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
External co-authors :
no
Language :
English
Title :
Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
Publication date :
May 2021
Event name :
International Conference on Software Engineering (ICSE 2021)
Event date :
from 23-05-2021 to 29-05-2021
Audience :
International
Main work title :
Proceedings of the 43rd International Conference on Software Engineering (ICSE 2021)
Pages :
847-859
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
Funders :
CE - Commission Européenne [BE]
Available on ORBilu :
since 09 February 2021

Statistics


Number of views
718 (71 by Unilu)
Number of downloads
289 (27 by Unilu)

Scopus citations®
 
8
Scopus citations®
without self-citations
2
WoS citations
 
6

Bibliography


Similar publications



Contact ORBilu