Distributed Hybrid Systems Compositionality and Reconfiguration for Distributed Hybrid Systems
Abstract:
The project pursues two major goals addressing the verification of cyber-physical systems. Firstly, one goal of this project is to develop theory, practice, and applications of verification techniques for distributed hybrid systems with flexible system structures that can change by reconfiguring the system. In order to address the crucial scalability issues of classical static hybrid systems verification we are developing a strictly compositional logic-based verification approach for these systems. In a breakthrough result, within this project we have developed a compositional verification logic for distributed hybrid systems that are subject to reconfig- urability [3]. Secondly, in a complementary dimension, we address the second analytic gap in cyber-physical system design. The continuous dynamics of system designs is fairly compli- cated for complex control systems. Today’s verification tools can only handle linear dynamics (or even only constant differential equations or inclusions). We developed symbolic invariant techniques for differential equations to analyze hybrid systems with more challenging nonlin- ear continuous dynamics. Both these extensions are implemented in our automated theorem prover KeYmaera [4]. KeYmaera has been used to verify a number of case studies. We studied the European Train Control System proved its safe functioning even in the context of per- turbations to the system dynamics [5]. Furthermore, we studied different highway maneuvers considering an a priori unbounded number of cars [1]. Increasing the degrees of freedom in the dynamics, we considered a factory automation scenario of a robot moving autonomously on a factory ground and studied the question whether it has a survival strategy by means of hybrid games [6]. Furthermore, we analyzed 2-D movement of robots. Here, we formally ver- ified different obstacle avoidance algorithms starting with static obstacles and then extending the scope to dynamic obstacles. In [2], we considered a class of distributed collision avoidance controllers designed to work even in environments with arbitrarily many aircraft or UAVs. We proved that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver without their knowledge.
References:
[1] Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified.
In: Butler, M., Schulte, W. (eds.) FM. LNCS, vol. 6664, pp. 42–56. Springer (2011)
[2] Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: Belta, C., Ivancic, F. (eds.) HSCC. pp. 125–130. ACM (2013)
[3] Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), 1–44 (2012), special issue for selected papers from CSL’10
[4] Platzer, A., Quesel, J.D.: KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando, A., Baum- gartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol. 5195, pp. 171–178. Springer (2008)
[5] Platzer, A., Quesel, J.D.: European train control system: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM. Lecture Notes in Computer Science, vol. 5885, pp. 246–265. Springer (2009)
[6] Quesel, J.D., Platzer, A.: Playing hybrid games with KeYmaera. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 7364, pp. 439–453. Springer (2012)
Submitted by Andre Platzer
on
Abstract:
The project pursues two major goals addressing the verification of cyber-physical systems. Firstly, one goal of this project is to develop theory, practice, and applications of verification techniques for distributed hybrid systems with flexible system structures that can change by reconfiguring the system. In order to address the crucial scalability issues of classical static hybrid systems verification we are developing a strictly compositional logic-based verification approach for these systems. In a breakthrough result, within this project we have developed a compositional verification logic for distributed hybrid systems that are subject to reconfig- urability [3]. Secondly, in a complementary dimension, we address the second analytic gap in cyber-physical system design. The continuous dynamics of system designs is fairly compli- cated for complex control systems. Today’s verification tools can only handle linear dynamics (or even only constant differential equations or inclusions). We developed symbolic invariant techniques for differential equations to analyze hybrid systems with more challenging nonlin- ear continuous dynamics. Both these extensions are implemented in our automated theorem prover KeYmaera [4]. KeYmaera has been used to verify a number of case studies. We studied the European Train Control System proved its safe functioning even in the context of per- turbations to the system dynamics [5]. Furthermore, we studied different highway maneuvers considering an a priori unbounded number of cars [1]. Increasing the degrees of freedom in the dynamics, we considered a factory automation scenario of a robot moving autonomously on a factory ground and studied the question whether it has a survival strategy by means of hybrid games [6]. Furthermore, we analyzed 2-D movement of robots. Here, we formally ver- ified different obstacle avoidance algorithms starting with static obstacles and then extending the scope to dynamic obstacles. In [2], we considered a class of distributed collision avoidance controllers designed to work even in environments with arbitrarily many aircraft or UAVs. We proved that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver without their knowledge.
References:
[1] Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified.
In: Butler, M., Schulte, W. (eds.) FM. LNCS, vol. 6664, pp. 42–56. Springer (2011)
[2] Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: Belta, C., Ivancic, F. (eds.) HSCC. pp. 125–130. ACM (2013)
[3] Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), 1–44 (2012), special issue for selected papers from CSL’10
[4] Platzer, A., Quesel, J.D.: KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando, A., Baum- gartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol. 5195, pp. 171–178. Springer (2008)
[5] Platzer, A., Quesel, J.D.: European train control system: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM. Lecture Notes in Computer Science, vol. 5885, pp. 246–265. Springer (2009)
[6] Quesel, J.D., Platzer, A.: Playing hybrid games with KeYmaera. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 7364, pp. 439–453. Springer (2012)