Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Checking correctness of transactional behaviors
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo
abstract:
The Signal Calculus is an asynchronous process calculus featuring multicast communication. It relies on explicit modeling of the communication structure of the network (communication flows), and on handling sessions, even multi-party. The calculus is strongly motivated by the practical needs of Service-Oriented Computing, and there exists a Java implementation, called JSCL, with a graphical modeling framework. To the aim of adding to SC (and JSCL) a verification environment, in this work we introduce the abstract semantics of SC, based on bisimulation. We show an example exploiting bisimilarity to prove the correctness of an SC model with respects to a transactional isolation requirement.
