Published: 14th December 2012|
|Invited Presentation: Conformance Testing of Interacting Components Marcello Bonsangue||1|
|Reducing Weak to Strong Bisimilarity in CCP Andrés Aristizábal, Filippo Bonchi, Luis Pino and Frank Valencia||2|
|Shared Contract-Obedient Endpoints Étienne Lozes and Jules Villard||17|
|Metric-Aware Secure Service Orchestration Gabriele Costa, Fabio Martinelli and Artsiom Yautsiukhin||32|
|Invited Presentation: Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications Ichiro Hasuo||47|
|Towards a Theory of Glue Simon Bliudze||48|
|Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations Kyriakos Poyias and Emilio Tuosto||67|
|Coherent Minimisation: Towards efficient tamper-proof compilation Dan R. Ghica and Zaid Al-Zobaidi||83|
|Interacting via the Heap in the Presence of Recursion Jurriaan Rot, Irina Măriuca Asăvoae, Frank de Boer, Marcello M. Bonsangue and Dorel Lucanu||99|
In component based software engineering, distributed components interact using complex coordination patterns that may be implemented by networks of communication channels. Channels receive stimuli from the environment possibly causing interactions to take place. In this talk I will introduce an execution model for channel based coordination, and present some principles and methods for testing implementations of coordination patterns to ensure their correct responses with respect to stimuli specifications.
*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 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:
 Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.
 Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. To appear in Proc. CAV 2012.