Keynote Speakers

Alessandro Abate, University of Oxford
Formal Verification and Control Synthesis of Complex Dynamic Systems: Model-Based and Data-Driven Methods
(slides)

Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large-scale, complex models, such as those needed in Cyber-Physical Systems (CPS) applications. Using data, which nowadays is becoming ever more accessible, has the potential to mitigate such limitations. However, this notoriously leads to a lack of formal proofs that are needed in safety-critical systems.
This talk covers research which addresses these shortcomings, by bringing model-based and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification.
In the first part of the talk, I will discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of systems with partly unknown dynamics. I will formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. I argue that the approach can be applied to complex physical systems (e.g., with spatially continuous variables), driven by external inputs and accessed under noisy measurements.
In the later part of the talk, I will concentrate on systems represented by models that are probabilistic with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear). Such stochastic hybrid models (SHS) are a natural mathematical framework for CPS. With focus on model-based verification procedures, I will provide algorithms for quantitative model checking of temporal specifications on SHS with formal guarantees. This is attained via the development of formal abstraction techniques based on quantitative approximations.
Theory is complemented by algorithms, all packaged in a software tool that is available to users, and applied in the domain of Smart Energy.

Franz-Josef Grosch, Robert Bosch GmbH
Elevate embedded real-time programming with a synchronous language.
(slides)

Product development at companies such as Bosch requires systems engineering for digital hardware and mechatronic components as well as software engineering for resource-constrained real-time applications cooperating with distributed server applications. While many of the involved engineering disciplines greatly benefit from model-based approaches and from advances in software infrastructures, deeply embedded software still is written in C since the seventies and runs on platforms designed in the nineties (e.g. OSEK). Simulation tools like Simulink or Modelica are used to test discrete code against continuous plant models or to generate code for certain aspects, but they do not really provide modern implementation technologies to address software architecture and qualities or to make embedded programming "attractive" for software professionals.
We regard synchronous languages as suitable to solve many of the issues in the integration (causality) and synchronisation (clocks) of time-triggered and event-triggered embedded functions that exhibit their behaviour over time steps and are coordinated according to their mode-switching in a structured synchronous control flow. Searching for an imperative synchronous language (with deterministic concurrent composition, and synchronous control flow), equipped with features for encapsulation and composition (objects, packages, separate compilation) and supporting programming parallel tasks deployed to separate cores (clock refinement and deterministic inter-task communication), we ended up in designing our own language, suitable for resource-constrained, real-time applications running on multi-core controllers.
We will explain the main requirements and features of this language, how they integrate with the principles of a synchronous language, how they can be applied to typical everyday problems in embedded development, and how such locally synchronous services may integrate in a globally asynchronous service architecture.

Thomas Henzinger, IST Austria
The Quest for Average Response Time
(slides)

Responsiveness -the requirement that every request to a system be eventually handled- is one of the fundamental liveness properties of a reactive system and lies at the heart of all methods for specifying and verifying liveness. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. The static computation of average response time has proved remarkably elusive even for finite-state models of reactive systems. We present, for the first time, a robust formalism that allows the specification and computation of quantitative temporal properties including average response time. The formalism is based on nested weighted automata, which can serve as monitors for measuring the response time of a reactive system. We show that quantitative properties specified by nested weighted automata can be computed in exponential space for nondeterministic finite-state models of reactive systems and in polynomial time for probabilistic finite-state models. The specific property of average response time can be computed in polynomial time in both cases.
This work is joint with Krishnendu Chatterjee and Jan Otop.