Reference : Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/46198
Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
English
Menghi, Claudio mailto [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 mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Briand, Lionel mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
In press
Proceedings of the 43rd International Conference on Software Engineering (ICSE 2021)
Yes
International
International Conference on Software Engineering (ICSE 2021)
from 23-05-2021 to 29-05-2021
[en] Monitors ; Languages ; Specification ; Validation ; Formal methods ; Semantics
[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.
University of Luxembourg: High Performance Computing - ULHPC ; Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
European Commission - EC
Researchers ; Professionals
http://hdl.handle.net/10993/46198
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
ThEodorE.pdfAuthor postprint264.54 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.