Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-32940-1_16 | CONCUR |
Keywords | Field | DocType |
semantic well-formedness,resulting theory,booking number,asynchronous specification,dynamic verification,concrete method,general semantic,asynchronous observation,stateful asynchronous property,asynchronous interaction,asynchronous semantics | Asynchronous communication,Computer science,Theoretical computer science,Stateful firewall,Java Modeling Language,Safety assurance,Database transaction,Semantics,Distributed computing | Conference |
Volume | ISSN | Citations |
7454 | 0302-9743 | 9 |
PageRank | References | Authors |
0.53 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tzu-Chun Chen | 1 | 90 | 4.03 |
| Kohei Honda | 2 | 698 | 29.60 |