. Rec and . Recpt, theAUT[i].recpt[0]; Cont_Aut[i]!j,m fi; fi; :: j=(j+1)%AUTNUM od } init{ /* Constant values obtained from the HMSC parsing *

]. B. Algayres, Y. Lejeune, F. Hugonment, and F. Hantz, The avalon project : a validation environment for sdl/msc descriptions, Proc. of SDL'93, pp.221-235, 1993.

R. Alur, G. J. Holzmann, and D. Peled, An analyser for mesage sequence charts, TACAS, pp.35-48, 1996.

R. Alur and M. Yannakakis, Model Checking of Message Sequence Charts, In CONCUR, pp.114-129, 1999.
DOI : 10.1007/3-540-48320-9_10

P. Baker, P. Bristow, C. Jervis, D. King, and B. Mitchell, Automatic Generation of Conformance Tests from Message Sequence Charts, In SAM, pp.170-198, 2002.
DOI : 10.1007/3-540-36573-7_12

N. Baudru and R. Morin, Synthesis of Safe Message-Passing Systems, FSTTCS, pp.277-289, 2007.
DOI : 10.1007/978-3-540-77050-3_23

H. Ben-abdallah and S. Leue, Syntactic detection of process divergence and non-local choice in message sequence charts, Proc. of TACAS'97, pp.259-274, 1997.
DOI : 10.1007/BFb0035393

D. Brand and P. Zafiropoulo, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, 1981.
DOI : 10.1145/322374.322380

B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun, Infinite-state high-level mscs : Model-checking and realizability, ICALP, pp.657-668, 2002.
DOI : 10.1007/3-540-45465-9_56
URL : https://hal.archives-ouvertes.fr/hal-00306255

L. Helouet, Sofat : Scenario formal analysis toolbox

L. Hélouët and C. Jard, Conditions for synthesis of communicating automata from hmscs, 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), 2000.

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

M. Mukund, K. N. Kumar, and M. Sohoni, Synthesizing distributed finitestate systems from mscs, In CONCUR, pp.521-535, 2000.
DOI : 10.1007/3-540-44618-4_37

A. Muscholl, D. Peled, and Z. Su, Deciding properties for message sequence charts, FoSSaCS, pp.226-242, 1998.

B. Selic, G. Gullekson, and P. T. Ward, Real-time object-oriented modelling, 1994.