TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 14122

Verification of Cyber-Physical Systems

( Mar 16 – Mar 21, 2014 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/14122

Organizers

Contact


Schedule

Motivation

The drastic reduction in the cost of sensing, actuating, computing and communication technology has enabled the proliferation of a new genre of engineered systems referred to as Cyber-Physical Systems, in which a network of embedded processors interacts closely with the physical world to achieve complex functionalities. Cyber-physical systems (CPS) are the systems of the future and are present in a wide range of applications in infrastructure, transportation, energy, health care, manufacturing, military, robotics and many others. A grand challenge is the development of a platform for building high-confidence CPS.

Model-based development has emerged as a de facto product development process in several domains, including automotive and aeronautics. The product development cycle starts with the mathematical modeling and analysis of the system, from which the code is generated either automatically or manually. This process has been successful in identifying bugs early in the design phase, thereby reducing development costs and time. Formal methods is an area of computer science that deals with mathematical methods for systems analysis. Our seminar will focus on the application of formal methods to CPS verification, mainly at the level of modeling, and will explore the connections of the same with implementation.

The convergence of computation, control and communication in CPS leads to networked hybrid system models, that is, networks of systems that exhibit mixed discrete-continuous behaviors. The seminar will bring together experts in the area of formal methods, hybrid control systems and real-time and embedded systems to foster discussion on topics including but not limited to:

  • Efficient and scalable techniques for verification of networked hybrid systems;
  • Unifying concepts from the discrete and continuous systems theory;
  • Bridging the gap between analysis at the model and implementation levels.

Tutorials, panels and break-out sessions will supplement our discussions to provide an overview of the state-of-the-art in the underlying areas and to identify specific problems and challenges.


Summary

Introduction

Cyber-physical systems are systems in which there exists a tight coupling between computation, communication and control. The drastic reduction in the cost of sensing, actuating, computing and communicating technology has enabled the proliferation of this new genre of engineered systems in which a network of embedded processors interact tightly with the physical world to achieve complex functionalities. They have applications in a wide-range of systems spanning communication, infrastructure, energy, health-care, manufacturing, military, robotics and transportation.

Cyber-physical systems are believed to be the systems of the future with an impact on the engineering systems technology comparable to the impact the internet had on the information systems. Governments around the world have taken several initiatives to exploit this potential. The report of the US President's Council of Advisors on Science and Technology (PCAST) has placed Cyber-Physical Systems on the top of the priority list for federal research investment. The European Union has recognized the strategic importance of Embedded Computing Systems and has launched the ARTEMIS Joint Technology Initiative (JTI) as part of the FP7 program. Also, the latest European Commission Work Programme 2013 for Information and Communication technologies identifies this with the Objective ICT-2013.3.4 dedicated to Advanced Computing, Embedded and Control systems.

Cyber-Physical Systems have immense potential for a long-term impact on the society. At the same time, the unprecedented complexity arising due to the interleaving of the cyber and the physical components is overwhelming. On one hand, digital systems operate is a discrete manner, where computation and communication proceed in synchronization with the processor cycles. On the other hand, physical systems execute continuously in dense real-time. Hence, cyber-physical systems are complex systems exhibiting both discrete and continuous behaviors, and are networked and/or distributed with possibly humans in the loop. The grand challenge of the near future is the development of design methodologies and tools to cater to the development of reliable cyber-physical systems.

Model-based development has emerged as the de facto product development process in several domains including automotive and aeronautics. Here, the product development cycle begins with an abstract mathematical model of the system which is subject to rigorous analysis. The code is then generated from the model either automatically or manually. This enables early detection and correction of bugs which in turn results in the reduction of development costs and time, thereby providing companies with a competitive edge. However, the techniques used for analysis based on simulation of the mathematical models is still ad hoc, and does not provide the high level of reliability guarantees expected out of safety-critical CPS. Formal verification is an alternative approach which aims to provide a proof of correctness of the system. It is a promising technique for achieving the goal of developing high confidence cyber-physical systems.

Outcomes of the seminar

The seminar focused on the challenges in the application of formal methods towards verification of CPS. The seminar had a total of 28 participants with a mix of computer scientists and control theorists.

Tutorials

Given the cross disciplinary nature of the seminar, 6 tutorials were arranged on the following topics to provide a common ground to enable researchers with different backgrounds to communicate.

  • Simulation-Based Techniques for the Falsification of Cyber-Physical Systems
  • Verification of Automotive Engine Control
  • Formal Methods for Control Design
  • On Optimal and Reasonable Control in the Presencve of Adversaries
  • Compositionality Results for Cardiac Cell Dynamics
  • Logic of Hybrid Games

Sessions

The following topics were identified as important issues in the application of formal verification to CPS. A separate session was dedicated to discuss the topics in the context of CPS.

  1. Simulation based methods: Application of simulation techniques for performing verification of CPS was discussed.
  2. Using verification for control design: This session focused on the application of formal verification techniques such as those based on abstractions for control design.
  3. Foundation of CPS: This session discussed the complexity and decidability of problems in verification and control of CPS.
  4. Applications: This session discussed the methods and challenges in the verification of aircraft control, biological systems and multi-robot path planning.
  5. Abstractions: This session discussed the issues regarding simplification techniques for scalable analysis of CPS.
  6. Lyapunov based methods: This session discussed notions of stability and techniques for their analysis.
  7. Constraint solving: Several verification problems can be formulated as constraint solving problems. This session discussed the challenges in constraint solving problems arising in CPS.
  8. Symbolic Verification: This session discussed problems related to building efficient algorithms and tools for symbolic state-space exploration.

Research Directions

The seminar successfully fostered communication between computer scientist and control theorist. Some challenges and research directions were identified such as the need for the development of compositional reasoning of CPS with multiple components and lightweight analysis methods to boost scalability (such as using simulation for verification).

Copyright Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar

Participants
  • Erika Abraham (RWTH Aachen, DE) [dblp]
  • Calin A. Belta (Boston University, US) [dblp]
  • Sergiy Bogomolov (Universität Freiburg, DE) [dblp]
  • Ken Butts (Toyota Research Institute North America- Ann Arbor, US) [dblp]
  • Xin Chen (RWTH Aachen, DE) [dblp]
  • Deepak D'Souza (Indian Institute of Science - Bangalore, IN) [dblp]
  • Thao Dang (VERIMAG - Grenoble, FR) [dblp]
  • Jyotirmoy Deshmukh (Toyota Technical Center - Gardena, US) [dblp]
  • Georgios Fainekos (Arizona State University - Tempe, US) [dblp]
  • Goran Frehse (VERIMAG - Grenoble, FR) [dblp]
  • Sebastian Gerwinn (Universität Oldenburg, DE) [dblp]
  • Radu Grosu (TU Wien, AT) [dblp]
  • Bruce H. Krogh (Carnegie Mellon University - Pittsburgh, US) [dblp]
  • Mircea Lazar (TU Eindhoven, NL) [dblp]
  • Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Oded Maler (VERIMAG - Grenoble, FR) [dblp]
  • Ian M. Mitchell (University of British Columbia - Vancouver, CA) [dblp]
  • Sayan Mitra (University of Illinois - Urbana Champaign, US) [dblp]
  • Richard M. Murray (CalTech - Pasadena, US) [dblp]
  • André Platzer (Carnegie Mellon University, US) [dblp]
  • Pavithra Prabhakar (IMDEA Software - Madrid, ES) [dblp]
  • Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
  • Harald Ruess (fortiss GmbH - München, DE) [dblp]
  • Indranil Saha (University of California - Berkeley, US) [dblp]
  • Sriram Sankaranarayanan (University of Colorado - Boulder, US) [dblp]
  • Konstantin Selyunin (TU Wien, AT) [dblp]
  • Danielle Tarraf (The Johns Hopkins University, US) [dblp]
  • Ashish Tiwari (SRI - Menlo Park, US) [dblp]
  • Mahesh Viswanathan (University of Illinois - Urbana-Champaign, US) [dblp]

Classification
  • modelling / simulation
  • semantics / formal methods
  • verification / logic

Keywords
  • Real-time
  • Embedded and Cyber-Physical Systems
  • Verification
  • Formal Methods
  • Control Systems
  • Hybrid Systems