From April 2 to May 3, 2013, LCCC will be hosting a focus period on Formal verification of Embedded Control Systems. The focus period will include a workshop with approximately 25 distinguished speakers, to be held at the Old Bishop's Palace, Lund, from April 17 to April 19, 2013.

Formal verification and validation (V&V) have been subject to research in controls, computer science, and networking but often in isolation from each other. With recent convergence of controls, computation, and communication into cyber-physical systems there is a need for unified theories and algorithms. Despite advances in V&V tools in respective areas, such unification is in its infancy. Moreover, rigorous V&V for systems of current interest is a complicated task due to common difficulties including the interaction between the software and the physical world, nontraditional information flow, modeling/environmental uncertainties, and unavoidable explosion of computational complexity of the currently available tools (in both domains). For example, model-based development of control systems makes it possible to verify the correctness of designs using simulation and formal methods before the control system is implemented. However, to be able to guarantee that the specifications also in the final software or hardware implementation is substantially more difficult due to, e.g., shared computing and communications resources, timing uncertainties, and partially open deployment platforms. At the workshop will focus on vertical verification covering both the control design level and the software artifact level. We believe that the success of formal methods and V&V in the intersection of controls, computer science, and networking is stringent on the development of truly hybrid methods that blend ideas from these areas and possibly others. The main purpose of the proposed LCCC workshop is to bring experts from academia, and industry together and promote exchange of ideas and establishment of interdisciplinary collaborations. A workshop with similar content was organized at Caltech by Richard Murray in 2009.

At any particular time, there will be room for up to 10 invited researchers. A typical visit will be 2-5 weeks. Interested visitors are encouraged to contact Karl-Erik Årzén <karlerik@control.lth.se>.

Scientific committee

Confirmed workshop speakers

Patricia Bouyer, LSV, CNRS - "Robust control for timed systems"
Calin Belta, Boston University - "Formal Methods for Discrete-Time Linear Systems"
Oded Maler, Verimag - "On Under-Determined Dynamical Systems"
Bruce Krogh, CMU - "Using Heterogeneous Formal Methods in Model-Based Development"
Alessandro Abate, TU Delft - "Computable analysis and control synthesis over complex dynamical systems via formal verification"
Gernot Heiser, Univ of New South Wales - "Towards Verified Real-World Systems"
Necmiye Ozay, Caltech - "Switching Protocols for Formal Composition of Low-level Dynamics in Cyber-physical Systems"
Marta Kwiatkowska, Oxford University - "Automatic Verification of Competitive Stochastic Systems"
Antoine Girard, Univ Joseph Fourier - "Symbolic control of incrementally stable systems"
Jean-François Raskin, Univ Libré de Bruxelles - "Energy and Mean-payoff games: extensions and variations"
Kim G. Larsen, Aalborg University - "Statistical Model Checking for Stochastic Hybrid Systems"
Susanne Graf, Verimag - "Knowledge for achieving distributed control"
Paulo Tabuada, UCLA - "Controller synthesis for linear systems and safe linear-time temporal logic"
Sanjit Seshia, University of California, Berkeley - "Quantitative Verification of Embedded Software"
Jyotirmoy Desmukh, Toyota US - "Mining Temporal Requirements of an Industrial-Scale Control System"
Ufuk Topku, University of Pennsylvania - "Synthesis of software-based control protocols for dynamically reconfigurable networks"
Holger Hermanns, University of Saarlands - "Stochastic, Hybrid and Real-Time Systems: From Foundations To Applications with Modest"
Andre Platzer, CMU - "Logical Analysis of Hybrid Systems"
Anders Rantzer, Lund University - "Formal Verfication of Dynamical Systems using Integral Quadratic Constraints"
Alberto Ferrari, ALES/UTC
Thomas Thelin, ABB - "Verification of a safety certified controller at ABB"

Visiting Scholars

Ebru Aydin Gol, Boston University
Ernst Moritz Hahn, Oxford University
Nikos Arechiga, Toyota
Sophie Quinton, TU Braunschweig
Ilya Tkachev, TU Delft
Erik Ramsgaard Wognsen, Aalborg University