Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review


Many security-related properties—such as non-interference—cannot be captured by traditional trace-based specification formalisms such as LTL. The reason is that they relate the events of two (or more) traces of the system, and LTL can only reason on one execution at a time. A number of hyper-property extensions of LTL have been proposed in the past few years, and case studies showing their ability to express interesting properties have also been shown. However, there has been less attention to hyper-properties for quantitative (timed) systems as well as very little work on developing a practically useful tool. Instead existing work focused on using ad-hoc implementations. In this paper we present a probabilistic hyper-property logic HPSTL for stochastic hybrid and timed systems and we show how to integrate the logic into existing statistical model checking tools. To show the feasibility of our approach we integrate the technique into a prototype implementation inside Uppaal SMC and apply it to the analysis of three side-channel attack examples. To our knowledge this is the first full implementation of a hyper logic inside a fully-fledged modelling environment.

Original languageEnglish
Title of host publicationModel Checking Software, SPIN 2022 : 28th International Symposium, SPIN 2022, Proceedings
EditorsOwolabi Legunsen, Grigore Rosu
Number of pages18
Publication date23 Aug 2022
ISBN (Print)978-3-031-15076-0
ISBN (Electronic)978-3-031-15077-7
Publication statusPublished - 23 Aug 2022
Event28th International Symposium on Model Checking of Software -
Duration: 21 May 202221 May 2022


Conference28th International Symposium on Model Checking of Software
Internet address
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals'. Together they form a unique fingerprint.

Cite this