, Correct-by-construction SR-systems

R. Ameur-boulifa, L. Henrio, O. Kulankhina, E. Madelaine, and A. Savu, Behavioural semantics for asynchronous components, Journal of Logical and Algebraic Methods in Programming, vol.89, pp.1-40, 2017.
URL : https://hal.archives-ouvertes.fr/hal-00761073

P. André, G. Ardourel, and C. Attiogbé, Composing Components with Shared Services in the Kmelia Model, 7th International Symposium on Software Composition, SC'08, vol.4954, 2008.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., Easycrypt: A tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01114366

A. Basu, B. 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.
URL : https://hal.archives-ouvertes.fr/hal-00722395

M. D. Bozga, V. Sfyrla, and J. Sifakis, Modeling Synchronous Systems in BIP, Proceedings of the Seventh ACM International Conference on Embedded Software, EMSOFT '09, pp.77-86, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00722479

S. Chabane, R. Ameur-boulifa, and M. Mezghiche, Rethinking of i/o-automata composition, Forum on Specification and Design Languages (FDL, pp.1-7, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01666415

A. Cohen, M. Duranton, C. Eisenbeis, C. Pagetti, F. Plateau et al., Synchronization of periodic clocks, Proceedings of the 5th ACM international conference on Embedded software, pp.339-342, 2005.
URL : https://hal.archives-ouvertes.fr/hal-01257295

J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu et al., Taming Heterogeneity -the Ptolemy Approach, Proceedings of the IEEE, vol.91, pp.127-144, 2003.

F. Fernandes and J. Royer, The STSLib project: Towards a formal component model based on STS, Electronic Notes in Theoretical Computer Science, vol.215, pp.131-149, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00416461

H. Garavel, F. Lang, and R. Mateescu, An overview of CADP, European Association for Software Science and Technology Newsletter, vol.4, pp.13-24, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00069920

. Kahn-gilles, The semantics of a simple language for parallel programming, vol.74, pp.471-475, 1974.

T. A. Henzinger, B. Horowitz, and C. M. Kirsch, Giotto: a time-triggered language for embedded programming, Proceedings of the IEEE, vol.91, issue.1, pp.84-99, 2003.

H. Kopetz, M. Braun, C. Ebner, A. Krüger, D. Millinger et al., The design of large real-time systems: The time-triggered approach, 16th IEEE Real-Time Systems Symposium, Palazzo dei Congressi, Via Matteotti, pp.182-187, 1995.

E. Lee, G. David, and . Messerschmitt, Static scheduling of synchronous data flow programs for digital signal processing, IEEE Transactions on computers, vol.100, issue.1, pp.24-35, 1987.

N. Lynch and M. Tuttle, An introduction to Input/Output automata, CWI-Quarterkly, vol.2, issue.3, pp.219-246, 1989.

R. Pacalet, M. Baclet, and A. Petit, Register transfer level simulation, 2004.

R. Mateescu and D. Thivolle, A model checking language for concurrent value-passing systems, FM 2008: Formal Methods, 15th International Symposium on Formal Methods, pp.148-164, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00315312

O. Müller and T. Nipkow, Combining model checking and deduction for i/o-automata, International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pp.1-16, 1995.

J. Sifakis, A framework for component-based construction extended abstract, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp.293-300, 2005.

, A Algorithme de construction des SR-modèles Nous introduisons d'abord les opérateurs et fonctions sur les listes qui sont utilisés dans l'algorithme 1

. L'opérateur, ¡ : s ¡ i efface l'indice i de la liste s

, L'opérateur : s iétend s avec un nouvel indice i

. L'opérateur, ? : s ? l incrémente les valeurs des indices de s. L'incrémentation est bornée par la valeur l (si s est vide alors s ? l retourne le tuple vide)

, La fonction fresh(s) crée un nouvelétat correspondantà la liste s. La fonction CreateTransition(s, ?, s ) : crée et retourne la transition s ? ? ? s

, La fonction greatest(s) renvoie la date la plus grande de la liste -correspondà la fonction lfst(s)

, La fonction greatest 2 (s) renvoie la deuxième date la plus grande de la liste. La fonction Exists.equiv(s, S) vérifie s'il existe unétatéquivalent de s dans S. La fonction S.equiv(s) retourne l'étatéquivalentà s dans S