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

• Type: Conference
• Year: 2008
• Where: FORTE
• Authors: Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo
• Keywords: Asynchronous Process Calculus, Formal Methods, FORTE 2008, Graphical Modeling Framework, Signal Calculus