Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications

Date: Thursday, June 21, 2012
Speaker: Ichiro Hasuo
Venue: IST Austria
Notes:

From 15:30

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—such as hybrid automaton or Platzer’s differential dynamic logic—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 discretejump 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 canrigorously 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.

Posted in RiSE Seminar