D. Simone and R. , Higher-level synchronising devices in Meije-SCCS, Theoretical Computer Science, vol.37, pp.245-267, 1985.
DOI : 10.1016/0304-3975(85)90093-3

K. G. Larsen, A context dependent equivalence between processes, Theoretical Computer Science, vol.49, pp.184-215, 1987.
DOI : 10.1007/bfb0015763

M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, vol.138, issue.2, pp.353-389, 1995.
DOI : 10.1016/0304-3975(94)00172-F
URL : https://doi.org/10.1016/0304-3975(94)00172-f

H. Lin, Symbolic transition graph with assignment, Concur'96, pp.50-65, 1996.
DOI : 10.1007/3-540-61604-7_47
URL : http://lcs.ios.ac.cn/~lhm/./papers/concur96.ps.gz

M. Hennessy and J. Rathke, Bisimulations for a calculus of broadcasting systems, Theoretical Computer Science, vol.200, issue.1-2, pp.225-260, 1998.
DOI : 10.1016/S0304-3975(97)00261-2
URL : https://doi.org/10.1016/s0304-3975(97)00261-2

L. Henrio, O. Kulankhina, D. Liu, and E. Madelaine, Verifying the correct composition of distributed components: Formalisation and Tool, Electronic Proceedings in Theoretical Computer Science, vol.6605, issue.3, 2014.
DOI : 10.1007/11783565_10
URL : https://hal.archives-ouvertes.fr/hal-01055370

L. Henrio, E. Madelaine, and M. Zhang, pNets: An Expressive Model for Parameterised Networks of Processes, 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing
DOI : 10.1109/PDP.2015.70
URL : https://hal.archives-ouvertes.fr/hal-01139432

L. Henrio, E. Madelaine, and M. Zhang, A Theory for the Composition of Concurrent Processes, Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
DOI : 10.1145/265943.265960
URL : https://hal.archives-ouvertes.fr/hal-01432917

D. Déharbe, Integration of SMT-solvers in B and Event-B development environments, Science of Computer Programming, vol.78, issue.3, pp.310-326, 2013.
DOI : 10.1016/j.scico.2011.03.007

D. Déharbe, P. Fontaine, Y. Guyot, and L. Voisin, Integrating SMT solvers in Rodin, Science of Computer Programming, vol.94, pp.130-143, 2014.
DOI : 10.1016/j.scico.2014.04.012

J. R. Abrial and S. Hallerstede, Refinement, decomposition, and instantiation of discrete models: Application to event-b, Fundamenta Informaticae, vol.77, issue.12, 2007.

C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovi? et al., Cvc4. In: Computer aided verification, 2011.

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, International Conference on Certified Programs and Proofs, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, International Symposium on Frontiers of Combining Systems, pp.12-27, 2011.
DOI : 10.1007/BFb0028402

A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber et al., Rigorous Component-Based System Design Using the BIP Framework, IEEE Software, vol.28, issue.3, pp.41-48, 2011.
DOI : 10.1109/MS.2011.27
URL : https://hal.archives-ouvertes.fr/hal-00722395

E. Baranov and S. Bliudze, Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP, Science of Computer Programming, vol.109, issue.0, pp.2-35, 2015.
DOI : 10.1016/j.scico.2015.05.011

P. Attie, E. Baranov, S. Bliudze, M. Jaber, and J. Sifakis, A general framework for architecture composability, Formal Aspects of Computing, vol.18, issue.2, pp.207-231, 2016.

R. Milner, Communication and Concurrency. Int. Series in Computer Science, 1989.

, ISO: Information Processing Systems ? Open Systems Interconnection ? LOTOS ? A Formal Description Technique based on the Temporal Ordering of Observational Behaviour, International Organisation for Standardization, vol.8807, 1989.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard: Version 2.6, 2017.

A. Mavridou, E. Stachtiari, S. Bliudze, A. Ivanov, P. Katsaros et al., Architecturebased design: A satellite on-board software case study, 13th Int. Conf. on Formal Aspects of Component Software, 2016.

S. Bliudze and J. Sifakis, The Algebra of Connectors???Structuring Interaction in BIP, IEEE Transactions on Computers, vol.57, issue.10, pp.1315-1330, 2008.
DOI : 10.1109/TC.2008.26
URL : https://hal.archives-ouvertes.fr/hal-00282866

S. Bliudze and J. Sifakis, Causal semantics for the algebra of connectors, Formal Methods in System Design, vol.204, issue.8, pp.167-194, 2010.
DOI : 10.1007/978-1-4471-0479-7

, AlgebraSort Action = new A lg eb r aS or t Im pl

, AlgebraSort Channel = new A lg e br aS o rt I mp l

, AlgebraSort Data = new A l ge br a So r tI mp l

, Emit, Action . addConstru ctor

, Receive, Action . addConstru ctor

, Action . addConstru ctor

, ( true ) --> t1 }, failure ( true )= failure ( b1 : sva_SV0 :1:1))/\( start ( true )= start, pp.0-1

, 13:1= fail ( b0 : sva_SV0 :1:1))/\(( b1 : sva_SV0 :1:1= b2 : sva_SV0 :1:1) /\(~( b1 : sva_SV0 :1:1\/ b2 : sva_SV0 :1:1)\/ b0 : sva_SV0 :1:1))

, resume ( false )= resume, pp.0-2

, \( resume ( false )= resume ( b2 : sva_SV1 :1:2))

, hb_B :16:2= resume ( b0 : sva_SV1 :1:2))/\(( b1 : sva_SV1 :1:2= b2, p.1

, ( b1 : sva_SV1 :1:2\/ b2 : sva_SV1 :1:2)\/ b0 : sva_SV1

, hb_B :118:6= finish )/\( finish =: ra :1:6) ,{} OT, pp.6-6

, failure ( false )= failure, pp.1-1

, \( start ( false )= start ( b2 : sva_SV0 :1:1))

, hb_B :13:1= fail ( b0 : sva_SV0 :1:1))/\(( b1 : sva_SV0 :1:1= b2 : sva_SV0 :1:1)

, b1 : sva_SV0 :1:1\/ b2 : sva_SV0 :1:1)\/ b0 : sva_SV0 :1:1)

, resume ( true )= resume ( b1 : sva_SV1 :1:2))/\( resume ( true )= resume, pp.1-2

, hb_B :16:2= resume ( b0 : sva_SV1 :1:2))/\(( b1 : sva_SV1 :1:2= b2, p.1

, b1 : sva_SV1 :1:2\/ b2 : sva_SV1 :1:2)\/ b0 : sva_SV1 :1:2)

, ( tick =: ra :1:3) ,{ t := (t -1)}

, hb_B :118:6= finish )/\( finish =: ra :1:6) ,{} OT, pp.6-6

, ra :1:4) ,{} OT, pp.4-6

, resume ( false )= resume, pp.0-2

, \( resume ( false )= resume ( b2 : sva_SV1 :1:2))

, hb_B :16:2= resume ( b0 : sva_SV1 :1:2))/\(( b1 : sva_SV1 :1:2= b2, p.1

, b1 : sva_SV1 :1:2\/ b2 : sva_SV1 :1:2)\/ b0 : sva_SV1 :1:2)

{. Ot, ra :1:5), pp.5-5

, hb_B :118:6= finish )/\( finish =: ra :1:6) ,{} OT, pp.6-6