http://www.dagstuhl.de/14122

16. – 21. März 2014, Dagstuhl Seminar 14122

Verification of Cyber-Physical Systems

Organisatoren

Rupak Majumdar (MPI-SWS – Kaiserslautern, DE)
Richard M. Murray (CalTech – Pasadena, US)
Pavithra Prabhakar (IMDEA Software – Madrid, ES)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Report, Volume 4, Issue 3 Dagstuhl Report
Motivationstext
Teilnehmerliste
Gemeinsame Dokumente
Programm des Dagstuhl Seminars [pdf]

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).

License
  Creative Commons BY 3.0 Unported license
  Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar

Classification

  • Modelling / Simulation
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

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

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.