Edition 2017: Automatic Synthesis of Controllers for Hybrid Systems
The School on Formal Methods for Cyber-Physical Systems addresses the foundations, techniques, and tools for analysis, verification, control, synthesis, implementation, and applications of cyber-physical systems (CPS).
Applications mainly deal with engineering and
natural systems, including signal circuits, robotics, automotive and avionics,
large-scale infrastructure networks, as well as biochemical and physiological
Topics of interest include, but are not limited to:
This first edition of the school has the goal of presenting the state of the art of the current techniques in controller synthesis for hybrid systems, to enable doctoral students and young researchers to advance the field and apply the developed methodologies to concrete scenarios promoting their application in the industrial practice.
The school is supported by grants from the PhD School in Natural Sciences and Engineering and the Department of Computer Science of the University of Verona.
The school is co-located with the Forum on specification & Design Languages (FDL 2017), to be held in Verona, 18-20 September 2017 (https://ecsi.org/fdl). Special arrangements will be provided to the participants to the school who register also to FDL (TBD).
add to your calendar
The airport of Verona is connected to the main European and national cities. From the airport you can reach the
city by taxi or by bus. A shuttle bus connects the airport to Verona Porta Nuova train station.
The train station of Verona Porta Nuova is connected with all the main Italian cities by fast and local trains. For the train schedule, please check the Italian railway company. From the station you can reach the Department of Computer Science by bus or by taxi.
Bus line 21 (towards S. Giovanni Lupatoto) get off at the first bus stop after Borgo Roma hospital; from the bus stop, you can see the department’s buildings. You can also catch bus line 22 (towards Policlinico/San Giovanni Lupatoto) and line 93 (during the night and on Sundays), towards Cadidavid. For these last two bus lines, get off at Borgo Roma hospital, then follow the map below. You can find timetables and line maps at the ATV website.
Take the A4 Milano-Venezia highway, exit Verona Sud then follow the direction "Ospedale Borgo Roma" (hospital), on the right. At the hospital, go straight, cross the small bridge on a river and take the second right. From here you can see the department buildings on your left.
Tutorial #7: 3 lectures + 1 laboratory
1. Temporal Planning and Execution with Uncertainty
2. Validation & Verification Issues in Planning & Scheduling
3. TGA-based Controllers for Robust Plan Execution
4. Hands-on laboratory: KEEN, PLATINUm and UPPAAL-TIGA
The design of safety critical and dependable Cyber Physical Systems (CPSs) is becoming increasingly important as technology advances. In fact, safety critical CPSs need to be certified and, thus, crucial properties require to be enforced. On the other hand, the need of meeting operational requirements in challenging real-world domains as, for instance, in robotics, often leads to the use of highly efficient software modules that address specific sub-parts of a larger problem with ad-hoc solving algorithms that cannot be easily verified. These lectures will provide an overview of Automated Planning and Scheduling (P&S) technology and its integration with Validation and Verification (V&V) techniques to synthesize autonomous control system for safety critical CPSs. The lectures will focus on a research initiative aiming at cascading a timeline-based planning system and a V&V technique based on Timed Game Automata (TGA) to automatically synthesize plan controllers. Also, we will present a tool for P&S Knowledge Engineering providing V&V features and guaranteeing robust execution.
Tutorial #1: 4 lectures
In these lectures, we aim at introducing the synthesis problem, as originally formulated by Church, and the solution given by Buechi and Landweber for specications in S1S (monadic second-order theory of one successor). Following a recent tutorial by Thomas, we will work out the solution in three main steps: (i) from S1S specications to Muller automata; (ii) from Muller automata to Muller games, and (iii) from Muller games to parity games. In the last part, we will provide a short account of variants and generalizations of the proposed solution.
Tutorial #5: 3 lectures + 1 laboratory
Many Cyber-physical systems are indeed Software Based Control Systems, that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model-Based Design approaches for automatic synthesis of control software for cyber-physical systems. We present algorithms, along with a tool implementing them (QKS), which from a formal model (as a Discrete-Time Hybrid System) of the controlled system (plant), implementation specifications (i.e., number of bits in the Analog-to-Digital, AD, conversion) and System-Level Formal Specifications (i.e., safety and liveness requirements for the closed-loop system) return correct-by-construction control software that has a Worst-Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. We show feasibility of the proposed approach by presenting experimental results on using it to synthesize control software for benchmark systems such as the buck DC-DC converter, a widely used mixed-mode analog circuit, and the inverted pendulum.
Tutorial: 3 lectures + 1 laboratory
Tutorial #6: 3 lectures
Problems of control engineering can be formulated as problems of control theory, solved, and the computed control law can be used to control the engineering system. Examples include: How to operate a robot arm to achieve a prespecified movement? How to control the movement of a robot in a corridor system? How to control a chemical process in a chemical reactor so that it completes a preset trajectory? Control problems with constraints on the state and on the input can be handled by the proposed framework. A piecewise-affine hybrid system on a polytope or on a simplex will be defined as a model of an engineering system. The control-to-facet problem concerns the control objective of transferring the state of the system from an initial state to a terminal state on a facet of the polytope. The solution of the problem yields a procedure on how to compute the control law of the continuous dynamics. The control law computes the input trajectory of the system, based on the state, so that the initial state of the system is transferred to any preferred state. This can be combined with a discrete control law which determines switches between discrete states so as to transfer the discrete state of the system to another discrete state. In case of partial observations, the state of the system is not observed but there are observations of a low-dimensional function of the state. The solution of the control problem in this case will also be shown. Extensions of the proposed framework will be discussed in the last lecture.
In this lecture we will look into a selection of
industrial design and verification problems arising in the development of
complex industrial cyber-physical systems, taken from the aerospace and HVAC commercial sectors.
Industrial systems pose challenging problems involving complex hybrid
non-linear dynamics including uncertainties. Solutions to these problems are bound to have dramatic
Partial solutions and demonstrated approaches
may represent important drivers for more aggressive endeavours in this important
Tutorial #4: 3 lectures + 1 laboratory
Hybrid automata model continuous-time systems whose state-space can be represented by a collection of continuous and discrete variables. In this tutorial, we will review the computational properties of various types of hybrid automata, in regard to their exact symbolic analysis and controller synthesis. We will then focus on the Linear Hybrid Automaton model and on algorithms based on symbolic manipulation of polyhedra. Towards the end of the tutorial we will learn how to answer controllability questions using a tool based on those algorithms.
Tutorial #3: 3 lectures + 1 laboratory
We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications on continuous-valued, discrete-time nonlinear control systems. To this end, we introduce a novel system relation termed feedback refinement relation to reason about the correctness of the closed loop. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation. In the hands-on tutorial, we will use SCOTS - an open source software tool - to apply the symbolic synthesis approach to solve several challenging control problems.
Tutorial #9: 2 lectures
1. Models of Timed Automata and Timed Finite State Machines (Davide Bresolin)
2. Synthesis of an Unknown Timed Finite State Machine (Nina Yevtushenko)
At the core of the modern synthesis challenges we find the managing of time-critical tasks, which are not completely under direct control of the system, and the scheduling of exclusive resources. Properties related to task durations as well as to the scheduling of resources may be naturally expressed in the simple yet powerful formalism of interval temporal logic, extended with a finite number of equivalence relations (usually one or two). In the lecture, we will lay the theoretical foundations of interval-based synthesis, we will showcase its expressive power, through a series of real-world examples, and we will describe a few basic results from the literature, together with the many interesting open problems related to it.
Tutorial #2: 4 lectures + 1 laboratory
While the seminal works on reactive synthesis were already published in the 70's, only recently, researcher began to look at how synthesis can be made more practical. For most specification logics, synthesis has a high computational complexity, and hence, the key issue is to avoid this complexity, either by using a simpler specification logic, or by employing a synthesis approach that is able to make use of specification properties that allow an efficient synthesis process and that are commonly found in specifications from practice. In these lectures, we will review such approaches and discuss how they can be applied in the presence of a plant model, as it is commonly the case in cyber-physical system control. A few practical exercises will round off the lectures.
View the social events of edition 2017.