Write a Blog >>
ICSE 2021
Mon 17 May - Sat 5 June 2021
Wed 26 May 2021 12:00 - 12:20 at Blended Sessions Room 3 - 2.1.3. Model Checking Chair(s): Oscar Dieste
Thu 27 May 2021 00:00 - 00:20 at Blended Sessions Room 3 - 2.1.3. Model Checking

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.

Wed 26 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:20 - 12:20
2.1.3. Model CheckingTechnical Track / Journal-First Papers at Blended Sessions Room 3 +12h
Chair(s): Oscar Dieste Universidad Politécnica de Madrid
11:20
20m
Paper
Adversarial Specification MiningJournal-First
Journal-First Papers
Hong Jin Kang , David Lo Singapore Management University
DOI Pre-print Media Attached
11:40
20m
Paper
Fast Parametric Model Checking through Model FragmentationTechnical Track
Technical Track
Xinwei Fang University of York, UK, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Faisal Alhwikem University of York, UK
Pre-print Media Attached
12:00
20m
Paper
Trace-Checking CPS Properties: Bridging the Cyber-Physical GapArtifact ReusableTechnical TrackArtifact Available
Technical Track
Claudio Menghi University of Luxembourg, Enrico Viganò University of Luxembourg, Domenico Bianculli University of Luxembourg, Lionel Briand University of Luxembourg and University of Ottawa
Pre-print Media Attached
23:20 - 00:20
23:20
20m
Paper
Adversarial Specification MiningJournal-First
Journal-First Papers
Hong Jin Kang , David Lo Singapore Management University
DOI Pre-print Media Attached
23:40
20m
Paper
Fast Parametric Model Checking through Model FragmentationTechnical Track
Technical Track
Xinwei Fang University of York, UK, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Faisal Alhwikem University of York, UK
Pre-print Media Attached
00:00
20m
Paper
Trace-Checking CPS Properties: Bridging the Cyber-Physical GapArtifact ReusableTechnical TrackArtifact Available
Technical Track
Claudio Menghi University of Luxembourg, Enrico Viganò University of Luxembourg, Domenico Bianculli University of Luxembourg, Lionel Briand University of Luxembourg and University of Ottawa
Pre-print Media Attached