10:45 - 12:45
Introduction
Tom Henzinger
Radu Grosu
Nikolaj Bjorner
14:00-15:30
Dejan Nickovic
Axel Legay
16:00-18:00
Oded Maler
Kim Larsen
Panel Discussion
Thomas Henzinger, IST Austria, Austria
Quantitative Reactive Modeling
Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria such as function, performance, cost, reliability, and robustness. For this purpose, we propose quantitative fitness measures for reactive models of concurrent and embedded systems. Besides measuring the "fit" between a system and a requirement numerically, the goal of the ERC project QUAREM (Quantitative Reactive Modeling) is to obtain quantitative generalizations of the paradigms on which the success of qualitative reactive modeling rests, such as compositionality, abstraction, model checking, and synthesis.
Radu Grosu, TU Wien, Austria
Uniform Lasso Sampling
In many practice-relevant applications, storing all states of a probabilistic system in memory is infeasible, and model checking tools break down. However, it is often the case that one can compute the successors of any given state in an efficient way. This opens up the door to sampling based approaches, which search the state space of the system for lassos offending the linear temporal property of interest. Unfortunately, such techniques are in general unable to sample the lasso space in a uniform way, which not only leads to inefficient search, but also hampers drawing any conclusion, in case no offending lasso is found. In this talk I will show that if one can (over)estimate the number of lassos in the system, one can devise a search technique that very accurately approximates uniform lasso sampling, with minimal memory requirements.
Nikolaj Bjorner, Microsoft Research, USA
Satisfiability Modulo Quantities: Beyond proofs and models in SMT solving
The talk describes past uses of Z3 for obtaining answers that are more than just an arbitrary proof or model. Several applications require good and models with certain characteristics: proofs that are colored for interpolation or models that are optimized with respect to an objective functions. I will examine tradeoffs of three main techniques used in applications: Encoding objective functions as part of the logical formulas, invoking Z3 multiple times with refined constraints, and it is also possible to formulate built-in solvers for optimization, in particular weighted Max-SMT. I will then outline the current organization of solvers in Z3 and directions we are taking to accommodate applications that require more than satisfiability.
Dejan Nickovic, Austrian Institute of Technology, Austria
Time for Mutants
Model-based testing is a popular technology for automatic and systematic test case generation, where a system-under-test (SUT) is tested for conformance with a model that specifies its intended behavior. Model-based mutation testing is a specific variant of model-based testing that is fault-oriented. In mutation testing, the test case generation is guided by a mutant, an intentionally altered version of the original model that specifies a common modeling error. We will present a mutation testing framework for real-time applications, where the model of the SUT and its mutants are expressed as timed automata. The framework is based on an algorithm for mutation-based real-time test case generation that uses symbolic bounded model checking techniques and incremental solving.
Axel Legay, INRIA/Irisa, France
PLASMA-lab: a Flexible, Distributable Statistical Model Checking Library
We present PLASMA-lab, a library that provides the functionality to create custom statistical model checkers based on arbitrary modelling languages -- users need only implement a few simple methods in a simulator class. PLASMA-lab is written in Java for maximum cross-platform compatibility and has already been incorporated in various performance-critical software and embedded hardware platforms. We have constructed a graphical user interface (GUI) that exposes the functionality of PLASMA-lab and facilitates its use as a stand-alone application with multiple modelling languages. The GUI adds the notion of projects and experiments, and implements a simple, practical means of distributing simulations using remote clients.
Oded Maler, CNRS-VERIMAG, France
Extending the Scope of Verification Thinking
Verification is essentially a collection of methods to reason about paths in large transition graph. Since it has been advertised for safety-critical or money-critical (circuits) systems, it is founded upon three implicit postulates:
In this talk I will explain how each of those should be relaxed in order to adapt verification technology to treat performance. An excellent question would be what remains of verification when all those are relaxed - I argue that compared to other disciplines that handle these issues (performance engineering, operations research) verification methodology provides more expressive (yet rigorous) tools to describe systems and behaviors.
Kim G. Larsen, Aalborg University, Denmark
Statistical Model Checking of Stochastic Hybrid Systems using UPPAAL-SMC
Timed automata, priced timed automata and energy automata have emerged as useful formalisms for modeling a real-time and energy-aware systems as found in several embedded and cyber-physical systems. Whereas the real-time model checker UPPAAL allows for efficient verification of hard timing constraints of timed automata, model checking of priced timed automata and energy automata are in general undecidable -- notable exception being cost-optimal reachability for priced timed automata as supported by the branch UPPAAL Cora. These obstacles are overcome by UPPAAL-SMC, the new highly scalable engine of UPPAAL, which supports (distributed) statistical model checking of stochastic hybrid systems with respect to weighted metric temporal logic. The talk will review UPPAAL-SMC and its applications to the domains of energy-harvesting wireless sensor networks, schedulability analysis for mixed criticality systems, as well as smart grids. In the talk I will also contemplate on how other b ranches of UPPAAL may benefit from the new scalable simulation engine of UPPAAL-SMC in order to improve their performance as well as scope in terms of the models that they are supporting. This includes application of UPPAAL-SMC to counter example generation, refinement checking, controller synthesis, optimization, testing and meta-analysis.