Sciweavers

Share
FORTE
2008

Checking Correctness of Transactional Behaviors

8 years 12 months ago
Checking Correctness of Transactional Behaviors
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 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. Keywords. Service Oriented Architectures, Event Notification, Coordination, Observational Equivalence
Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guan
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2008
Where FORTE
Authors Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo
Comments (0)
books