Supported by the Norwegian Research Council FORSTERK-project COEMS Training Network
.
Runtime Verification of Streams with TeSSLa
We present the TeSSLa Temporal Stream-based Specification Language (https://www.tessla.io). It can analyze the behavior of cyber-physical systems, where timing is a critical issue. TeSSLa is ideally suited for stream runtime verification (SRV) and comes with tools supporting this goal. TeSSLa supports timestamped events natively and is hence suitable for streams that are both sparse and fine-grained.
In addition to an overview and short example on the language and tools, we’ll apply TeSSLa and its associated tools that have been developed in the COEMS EU H2020 project to analyze data races.
Gray-box Monitorability of Hyperproperties – the Case of Data Minimization
Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. However, black-box monitoring of HyperLTL is not possible in general.
In this tutorial, I will present an alternative approach called gray-box monitoring which combines runtime verification and static analysis to cover a wider class of hyperproperties.
The tutorial will start with a recap of some basic results about black-box monitoring LTL and Hyper-LTL. I will then sketch a proof that black-box monitoring HyperLTL formulas with quantifier alternations is unfeasible in general, and present a gray-box approach to circumvent this limitation. Gray-box monitoring involves the use of static information about a system at run-time, which changes the monitoring problem and introduces new challenges. Thus, I will present a refined notion of monitorability, both for trace properties and hyperproperties, that takes into account static knowledge and computability of the monitor.
In the second part of the tutorial, I will present a case study where this approach is applied to monitor a privacy hyperproperty called distributed data minimality. The case-study is supported by a proof-of-concept implementation that uses the KeY symbolic execution engine and the Z3 SMT solver to perform static analysis at runtime.
This tutorial is based on joint work with César Sánchez, Gerardo Schneider and Borzoo Bonakdarpour.
Qualitative and Quantitative Specification-based Monitoring of Cyber-Physical Systems
The term Cyber-Physical Systems (CPS) typically refers to engineered, physical and biological systems monitored and/or controlled by an embedded computational core. The behaviour of a CPS over time is generally characterised by the evolution of physical quantities, and discrete software and hardware states. In general, these can be mathematically modelled by the evolution of continuous state variables for the physical components interleaved with discrete events. Despite large effort and progress in the exhaustive verification of such hybrid systems, the complexity of CPS models limits formal verification of safety of their behaviour only to small instances. An alternative approach, closer to the practice of simulation and testing, is to monitor and to predict CPS behaviours at simulation-time or at runtime. In this lecture, we introduce the state-of-the-art techniques for qualitative and quantitative monitoring of CPS behaviours.
Runtime verification for rigorous engineering of cyber-physical systems
Cyber-physical systems (CPS) combine computational and physical components that interact with their sophisticated and unpredictable environments via sensors and actuators. Exhaustively evaluating correctness and robustness of CPS is often intractable. Runtime verification (RV) is a more pragmatic method that combines formal specifications with the analysis of individual system behaviors. RV for CPS has been a vivid area of research in the recent past and there is a plethora of powerful methods and tools for monitoring CPS. But can we use these monitors to go beyond RV?
In this lecture, I will present a number of methods that support rigorous engineering of CPS and that use RV as their core technology. I will sketch procedures for pattern matching, predictive monitoring, search-based testing, parameter synthesis, specification mining, and trace and system diagnostics. I will use these procedures to demonstrate the extraordinary versatility of the RV technology and its application during the design and operation of CPS.
Monitoring with Data
Runtime Verification techniques can be broadly split into those that view execution traces as sequences of (possibly timestamped) atomic symbols and those that view them as sequences of events with richer structure. This has an impact on the specification languages and the monitoring algorithms used. In this talk I give an overview of the main methods within Runtime Verification for handling the second case, which we may refer to as parametric or first-order RV, and discuss the main challenges when applying such methods in practice. A core technique discussed in detail is that of parametric trace slicing as popularised by the JavaMOP tool and later utilised extensively in my MarQ tool.
A Flight Rule Checker for the LADEE Lunar Spacecraft(Wednesday, part of the ICTAC keynotes)