Document Actions

Design and Analysis of Cyber-Physical Systems (Seminar)

The development of cyber physical systems (CPS) is considered to be the next computing revolution. Cyber physical systems are networked computational systems that interact with the physical world. Examples of such systems are autonomous cars, robots, intelligent energy-efficient buildings, embedded medical devices, etc. The systems like that require tight connection between discrete and continuous behavior. The design of CPS presents many challenges because of their complexity, safety requirements and real-time nature. Thus collaboration among people from different disciplines and between academics and industry is required to make progress in the area of CPS.

In this seminar we will discuss how to model, understand and verify CPS, what are the challenges to guarantee they behave safely and adapt to their environment. Furthermore we will outline open questions and research challenges in the area of CPS.

The topics of the seminar are primarily based on the papers below.

Please register using the Moodle e-Learning Platform (IIF username and WWW password required).

Introductory literature

Introduction to Cyber Physical Systems

1. John A. Stankovic et al., Challenges and Opportunities of Physical Computing Systems, IEEE Computer, Nov 2005.

2. Insup Lee et al., High-Confidence Medical Device Software and Systems

3. Edward A. Lee, Cyber-Physical Systems - Are Computing Foundations Adequate?

4. Jeannette M. Wing, Cyber-Physical Systems Research Charge

5. Edward A. Lee, Cyber Physical Systems: Design Challenges

Introduction to Hybrid Automata

1. Thomas A. Henzinger, The Theory of Hybrid Automata.

2. Karl Henrik Johansson, Hybrid Systems Course, 2000, Berkeley.

3. Claire Tomlin, Hybrid Systems: Modeling, Analysis, and Control Course Spring 2004, Stanford

4. Rajeev Alur, Minicourse on Hybrid Systems: Modeling and Verification, Presented at Dynamics and Verification Workshop, Brusells, July 2001

5. John Lygeros, Lecture Notes on Hybrid Systems, 2004

6. J. Lygeros, C. Tomlin and S. Sastry Art of Hybrid Systems, Compendium of Lecture Notes for the Hybrid Systems Class, 2002.

7. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.H., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, Y.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138:3-34, 1995.

8. Ansgar Fehnker, Franjo Ivancic, Benchmarks for Hybrid Systems Verification, HSCC 2004

9. R. Alur, T.A. Henzinger, P.-H. Ho. Automatic symbolic verification of embedded systems, IEEE Trans. on Software Engineering 22(3):181-201, 1996.

10. Raymond A. DeCarlo, Michael S. Branicky, Stefan Pettersson, Bengt Lennartson, Perspectives and Results on the Stability and Stabilizability of Hybrid Systems , Proceedings of IEEE, Special Issue on Hybrid Systems, July 2000.

Papers to prepare the presentation on

Hybrid Modeling - Reachability Analysis - Safety Verification

1. C. Tomlin, I. Mitchell, A. Bayen, and M. Oishi, Computational Techniques for the Verification and Control of Hybrid Systems, Proceedings of the IEEE, Volume 91, Number 7, pp. 986-1001, July 2003.

2. Claire Tomlin, John Lygeros, and Shankar Sastry, A Game Theoretic Approach to Controller Design for Hybrid Systems , Proceedings of the IEEE, Volume 88, Number 7, July 2000.

3. Stefan Ratschan, Zhikun She, Safety verification of hybrid systems by constraint propogation-based abstraction refinement, 2007

4. Stefan Ratschan, Zhikun She, Constraints for Continuous Reachability in the Verification of Hybrid Systems, AISC 2006

5. Oded Maler, Gregory Batt, Approximating Continuous Systems by Timed Automata, FMSB 2008

6. O. Stursberg, S. Kowalewski, S. Engell, On the Generation of Timed Discrete Approximations for Continuous Systems, Mathematical and Computer Modelling of Dynamical Systems, 2000, Vol. 6, No. 1, pp. 51-70.

7. O. Stursberg, S. Kowalewski, S. Engell , Timed Approximations of Hybrid Processes for Controller Verification, IFAC 1999

8. Stephen Prajna, Ali Jadbabaie, Safety Verification of Hybrid Systems using Barrier Certificates, HSCC 2004

9. Werner Damm, Hardi Hungar, Ernst-Rudiger Olderog,Verification of Cooperating Traffic Agents, FMCO 2003: 77-110.

10. Lincoln, P. and Tiwari, A., Symbolic systems biology: Hybrid modeling and analysis of biological networks, Hybrid Systems: Computation and Control, HSCC 2004, Lecture Notes in Computer Science 2993, 660-672.

Hybrid System Stability

1. Jens Oehlerking, Henning Burchardt, Oliver E. Theel, Fully Automated Stability Verification for Piecewise Affine Systems, HSCC 2007

2. Jens Oehlerking, Oliver Theel, Decompositional Construction of Lyapunov Functions for Hybrid Systems, HSCC 2009

3. Stephane Devismes, Sebastien Tixeuil, Masafumi Yamashita, Weak vs. Self vs. Probabilistic Stabilization, ICDCS 2008: 681-688

The seminar will be a block course and take place at the Fachschaftshaus Schauinsland.

Instructors: Andreas Podelski | Sergiy Bogomolov | Corina Mitrohin
Times & Locations: The seminar will be a block course and take place at the Fachschaftshaus Schauinsland. Kick-off meeting will be on Friday, the 23th of October, at 10:00 in room 052-00-016. Also you can send us (Sergiy Bogomolov or Corina Mitrohin) an e-mail and we will make an appointment with you.