J. C. Baeten and W. Wejland, Process Algebra, 1990.

L. Bettini, M. Coppo, L. D-'antoni, M. De-luca, M. Dezani-ciancaglini et al., Global Progress in Dynamically Interleaved Multiparty Sessions, CONCUR'08, pp.418-433, 2008.
DOI : 10.1007/978-3-540-85361-9_33

L. Bocchi, C. Laneve, and G. Zavattaro, A Calculus for Long-Running Transactions, FMOODS, pp.124-138, 2003.
DOI : 10.1016/0890-5401(92)90008-4

M. Boreale, R. Bruni, R. Nicola, and M. Loreti, Sessions and Pipelines for Structured Service Programming, Formal Methods for Open Object- Based Distributed Systems, pp.19-38, 2008.
DOI : 10.1007/978-3-540-68863-1_3

M. Bravetti and G. Zavattaro, On the expressive power of process interruption and compensation, Mathematical Structures in Computer Science, vol.4960, issue.03, pp.565-599, 2009.
DOI : 10.1007/s10270-006-0012-1

S. Capecchi, E. Giachino, Y. , and N. , Global escape in multiparty sessions, FSTTCS'10, pp.338-351, 2010.
DOI : 10.1007/978-3-540-78739-6_21
URL : https://hal.archives-ouvertes.fr/hal-00909314

M. Carbone, Session-based Choreography with Exceptions, Electronic Notes in Theoretical Computer Science, vol.241, pp.35-55, 2009.
DOI : 10.1016/j.entcs.2009.06.003

M. Carbone, K. Honda, Y. , and N. , Structured Interactional Exceptions in Session Types, 19th International Conference on Concurrency Theory (Concur'08), pp.402-417, 2008.
DOI : 10.1007/978-3-540-85361-9_32

M. Carbone, K. Honda, N. Yoshida, R. Milner, G. Brown et al., A theoretical basis of communication-centred concurrent programming, 2006.

C. Filho, F. Romanovsky, A. , R. , and C. M. , Improving reliability of cooperative concurrent systems with exception flow analysis, Journal of Systems and Software, vol.82, issue.5, pp.874-890, 2009.
DOI : 10.1016/j.jss.2008.12.015

R. Demangeon and K. Honda, Nested Protocols in Session Types, Lecture Notes in Computer Science, vol.7454, pp.272-286, 2012.
DOI : 10.1007/978-3-642-32940-1_20

P. Deniélou and N. Yoshida, Buffered Communication Analysis in Distributed Multiparty Sessions, CONCUR'10, pp.343-357, 2010.
DOI : 10.1007/978-3-642-15375-4_24

S. Gay and M. Hole, Subtyping for session types in the pi calculus, Acta Informatica, vol.Analysis, issue.1, pp.191-225, 2005.
DOI : 10.1007/s00236-005-0177-z

K. Honda, R. Hu, R. Neykova, T. Chen, R. Demangeon et al., Structuring Communication with Session Types, COB'12, Lecture Notes in Computer Science, 2012.
DOI : 10.1007/11423348_10
URL : https://hal.archives-ouvertes.fr/hal-01213679

K. Honda, A. Mukhamedov, G. Brown, T. Chen, Y. et al., Scribbling Interactions with a Formal Foundation, ICDCIT 2011, 2011.
DOI : 10.1007/978-3-642-19056-8_4

K. Honda, V. T. Vasconcelos, and M. Kubo, Language primitives and type discipline for structured communication-based programming, ESOP'98, pp.22-138, 1998.
DOI : 10.1007/BFb0053567

K. Honda, N. Yoshida, and M. Carbone, Multiparty asynchronous session types, POPL'08, pp.273-284, 2008.

R. Hu, D. Kouzapas, O. Pernet, N. Yoshida, and K. Honda, Type-Safe Eventful Sessions in Java, ECOOP'10, pp.329-353, 2010.
DOI : 10.1007/978-3-642-14107-2_16

R. Hu, R. Neykova, N. Yoshida, D. , and R. , Practical Interruptible Conversations, 4th International Conference on Runtime Verification, Lecture Notes in Computer Science, 2013.
DOI : 10.1007/978-3-642-40787-1_8
URL : https://hal.archives-ouvertes.fr/hal-01146168

R. Hu, N. Yoshida, and K. Honda, Session-Based Distributed Programming in Java, ECOOP'08, pp.516-541, 2008.
DOI : 10.1007/978-3-540-70592-5_22

S. Jak?i´jak?i´c and L. Padovani, Exception Handling for Copyless Messaging, Proceedings of the 14th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'12), pp.151-162, 2012.

I. Lanese and F. Montesi, Error Handling: From Theory to Practice, Leveraging Applications of Formal Methods, Verification, and Validation, pp.66-81, 2010.
DOI : 10.1007/978-3-642-16561-0_13

I. Lanese, C. Vaz, and C. Ferreira, On the Expressive Power of Primitives for Compensation Handling, ESOP, pp.366-386, 2010.
DOI : 10.1007/978-3-642-11957-6_20

A. Lapadula, R. Pugliese, and F. Tiezzi, A Calculus for Orchestration of Web Services, ESOP, pp.33-47, 2007.
DOI : 10.1007/978-3-540-71316-6_4

C. Lewerentz and T. Lindner, Formal Development of Reactive Systems -Case Study Production Cell, 1995.

R. Neykova, N. Yoshida, and R. Hu, SPY:Local Verification of Global Protocols, 4th International Conference on Runtime Verification, 2013.

C. M. Rubira, R. De-lemos, G. R. Ferreira, and F. C. Filho, Exception handling in the development of dependable component-based systems, Software: Practice and Experience, vol.22, issue.3, pp.195-236, 2005.
DOI : 10.1002/spe.632

C. M. Rubira and Z. Wu, Fault tolerance in concurrent object-oriented software through coordinated error recovery, FTCS '95: Proceedings of the Twenty-Fifth International Symposium on Fault-Tolerant Computing, p.499, 1995.

K. Takeuchi, K. Honda, and M. Kubo, An interaction-based language and its typing system, PARLE'94, pp.398-413, 1994.
DOI : 10.1007/3-540-58184-7_118
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1431

F. Tartanoglu, V. Issarny, A. Romanovsky, and N. Levy, Coordinated forward error recovery for compositeweb services, Reliable Distributed Systems, IEEE Symposium, p.167, 2003.

H. T. Vieira, L. Caires, and J. C. Seco, The Conversation Calculus: A Model of Service-Oriented Computation, ESOP, pp.269-283, 2008.
DOI : 10.1007/978-3-540-78739-6_21

J. Xu, A. Romanovsky, R. , and B. , Coordinated exception handling in distributed object systems: from model to system implementation, Proceedings. 18th International Conference on Distributed Computing Systems (Cat. No.98CB36183), pp.12-21, 1998.
DOI : 10.1109/ICDCS.1998.679465

A. Appendix, Semantics In this section we show the semantics of our Client-Seller-Bank protocol. First we recall the syntax by adding details about C-B interaction (Figure 13) B refreshes the offer every n-seconds, where n is the value of timeout. The process iterates until an agreement is reached. The time intervals are modelled through a timer construct ( let h = timer(0) in . . .). Thus there are two iterations in the process: one related to the deal (def X) and the other used by B to iterate on time intervals (def Y ). C examines B offer and, if she agrees on it, she throws an exception to exit the iteration