Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

ChenH12 (In proceedings)
Author(s) Tzu-Chun Chen and Kohei Honda
Title« Specifying Stateful Asynchronous Properties for Distributed Programs »
InCONCUR
SeriesLecture Notes in Computer Science
Volume7454
Page(s)209-224
Year2012
PublisherSpringer
ISBN number978-3-642-32939-5
URLhttp://www.di.unito.it/~chen/papers/CONCUR_2012.pdf
Abstract
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 transaction, 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 characterise the class of specifications suitable for verifications through asynchronous interactions. The resulting theory offers a general semantic setting as well as concrete methods to analyse 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.

Download the complete article: CONCUR_2012.pdf

BibTeX code

@inproceedings{ChenH12,
  volume = {7454},
  author = {Tzu-Chun Chen and Kohei Honda},
  series = {Lecture Notes in Computer Science},
  booktitle = {CONCUR},
  url = {http://www.di.unito.it/~chen/papers/CONCUR_2012.pdf},
  title = {Specifying Stateful Asynchronous Properties for Distributed
           Programs},
  isbn = {978-3-642-32939-5},
  tag = {CONCUR 2012},
  abstract = {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 transaction, 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 characterise the class of specifications suitable for
              verifications through asynchronous interactions. The resulting
              theory offers a general semantic setting as well as concrete
              methods to analyse 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.},
  localfile = {http://www.di.unito.it/~chen/papers/CONCUR_2012.pdf},
  publisher = {Springer},
  year = {2012},
  pages = {209-224},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!