ABSTRACT. A calculus is defined by the abstract syntax of its terms, together with axioms and rules that define its semantics. In a programming calculus, the terms are classified into four sorts, program specifications, program designs, the programs themselves, and their traces (logs of execution behaviour). The axioms are familiar algebraic equations, together with an ordering relation for valid transformation (refinement) of terms. Additionally, logical proof rules permit conditional algebraic calculations. The axioms apply equally to specifications, designs, programs and traces. Each sort includes all terms of the following sort. Refinement permits optimisation of terms within each sort, or derivation of a terms by stepwise refinement and decomposition from its preceding sorts. A trace is a constant term that cannot be further refined. It is most frequently generated automatically by running the program on a correct implementation of the calculus. The calculus detects faults in the implementation, distinguishing them clearly from faults due to programming errors.

ABSTRACT. Hyperproperties relate multiple computation traces to each other. Information-flow control is a prominent application area. Observational determinism, for example, is a hyperproperty which states that two executions agree on the observable output whenever they agree on the observable input, i.e., private data does not influence the observable behavior of the system. Standard trace monitoring techniques are not applicable to such properties: For example, a violation of observational determinism cannot be determined by analyzing executions in isolation, because each new execution must be compared to executions already seen so far. In this tutorial, we will present recent algorithmic advances in monitoring hyperproperties. We will present several optimization techniques and illustrate them on practical examples and demos of RVHyper, a runtime verification tool for hyperproperties.

ABSTRACT. The tutorial session will introduce ideas centered around robustness of temporal specifications and the use of these ideas to solve important problems. Robustness of specifications extends the Boolean valuation of properties over runtime traces to real-valued semantics. These semantics turn out to be incredibly useful for Cyber-Physical Systems such as falsification for finding property violations in black-box models; parameter mining for synthesizing model parameters and requirements; and runtime monitoring. The tutorial will include an in-depth demonstration of the S-TaLiRo tool on several benchmark problems from the automotive and medical device industries.

ABSTRACT. In  stream-based runtime monitoring, streams of data, called input streams, which involve data collected from the system at runtime, are  translated into new streams of data, called output streams, which define statistical measures and verdicts on the system based on the input data. The advantage of this setup is an easy-to-use and modular way for specifying monitors with rich verdicts, provided  with formal  guarantees on the complexity of the monitor. 

In this tutorial, we give an overview of the different classes of stream specification languages, in particular those with real-time features.  With the help of the real-time stream specification language RTLola, we illustrate which features are necessary for the definition of the various types of real-time properties and we discuss how these features need to be implemented in order to guarantee memory efficient and reliable monitors.
To demonstrate the expressive power of the different classes of stream specification languages and the complexity of the different features, we use a series of examples  based on our experience with monitoring problems from  the areas of unmanned aerial systems and telecommunication networks. 

ABSTRACT. Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior on systems at runtime. In this tutorial, we are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred to as timed properties. First, we present a taxonomy of the main principles and concepts involved in the runtime enforcement of timed properties. Then, we overview a theoretical framework for the enforcement where timed properties are described by timed automata and feature uncontrollable events. Then, we present some tools for runtime enforcement, and two tools dedicated to timed properties. Finally, we present some open challenges and avenues for future work.

ABSTRACT. In  stream-based runtime monitoring, streams of data, called input streams, which involve data collected from the system at runtime, are  translated into new streams of data, called output streams, which define statistical measures and verdicts on the system based on the input data. The advantage of this setup is an easy-to-use and modular way for specifying monitors with rich verdicts, provided  with formal  guarantees on the complexity of the monitor. 

In this tutorial, we give an overview of the different classes of stream specification languages, in particular those with real-time features.  With the help of the real-time stream specification language RTLola, we illustrate which features are necessary for the definition of the various types of real-time properties and we discuss how these features need to be implemented in order to guarantee memory efficient and reliable monitors.
To demonstrate the expressive power of the different classes of stream specification languages and the complexity of the different features, we use a series of examples  based on our experience with monitoring problems from  the areas of unmanned aerial systems and telecommunication networks. 

ABSTRACT. Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior on systems at runtime. In this tutorial, we are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred to as timed properties. First, we present a taxonomy of the main principles and concepts involved in the runtime enforcement of timed properties. Then, we overview a theoretical framework for the enforcement where timed properties are described by timed automata and feature uncontrollable events. Then, we present some tools for runtime enforcement, and two tools dedicated to timed properties. Finally, we present some open challenges and avenues for future work.