JFLI Seminar on Cyber-Physical System Verification

Date: Wednesday June 8, 2016

Time: 15:00

Place: room 007, Faculty of Science Bldg. 7, Hongo Campus, The University of Tokyo

Title:  Nonstandard Static Analysis: a (Meta-)Logical Approach in Cyber-Physical System Verification

Speaker:   Ichiro Hasuo (Dept. Computer Science, The University of Tokyo)

Abstract:  *Hybrid systems* are those which exhibit both discrete « jump » and continuous « flow » dynamics. Their importance—as components of *cyber-physical systems*—is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers. There are naturally two directions towards the study of hybrid systems: *control theory* (typically continuous) and *formal verification* (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous « flow » dynamics. Many existing techniques include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations. In our project we take a different path of *turning flow into jump*—more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we can rigorously speak about infinites and infinitesimals. In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover. The talk is based on the joint work with Kohei Suenaga, Kyoto University. References: [1] Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011. [2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. Proc. CAV 2012.


Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *