Constraint-based Monitoring of Hyperproperties
Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. It is necessary to store previously seen traces, because every new incoming trace needs to be compatible with every system run observed so far. Furthermore, the new incoming trace poses requirements on future traces. In our monitoring approach, we focus on those requirements by rewriting a hyperproperty in the temporal logic HyperLTL to a Boolean constraint system. A hyperproperty is then violated by multiple runs of the system if the constraint system becomes unsatisfiable. We compare our implementation, that utilizes either BDDs or a SAT solver to store and evaluate constraints, to the automata-based monitoring tool RVHyper.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | Monitoring and Runtime VerificationTACAS at SUN I Chair(s): Ondřej Lengál Brno University of Technology | ||
16:30 30mTalk | Specification and Efficient Monitoring Beyond STL TACAS Link to publication | ||
17:00 30mTalk | VyPR2: A Framework for Runtime Verification of Python Web Services TACAS Joshua Dawes University of Manchester and CERN, Giles Reger University of Manchester, Giovanni Franzoni , Andreas Pfeiffer , Giacomo Govi Link to publication | ||
17:30 30mTalk | Constraint-based Monitoring of Hyperproperties TACAS Link to publication |