Sep 06, 2012

Tzu-Chun Chen, Kohei Honda

Specifying stateful asynchronous properties for distributed programs (CONCUR 2012)

Having stateful specifications to track the states of processes, such as the balance of a customer for online shopping or the booking number of a trans- action, is needed to verify real-life interacting systems. For safety assurance of distributed IT infrastructures, specifications need to capture states in the presence of asynchronous interactions. We demonstrate that not all specifications are suitable for asynchronous observations because they implicitly rely on an order- preservation assumption. To establish a theory of asynchronous specifications, we use the interplay between synchronous and asynchronous semantics, through which we characterize the class of specifications suitable for verifications through asynchronous interactions. The resulting theory offers a general semantic setting as well as concrete methods to analyze and determine semantic well-formedness (healthiness) of specifications with respect to asynchronous observations, for both static and dynamic verifications. In particular, our theory offers a key criterion for suitability of specifications for distributed dynamic verifications.

Full Report

The full report of the paper.

Slides

The slides for the talk.

Please reload

Call

T: (+49) 06151-16-27813