R. Alur and D. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

C. Aussagù-es and V. David, A method and a technique to model and ensure timeliness in safety critical real-time systems, 4th Intl. Conf. Engineering of Complex Computer Systems (ICECCS '98), pp.2-12, 1998.

N. Azmy, S. Merz, C. Weidenbach, . Tla, and Z. Vdm, A Rigorous Correctness Proof for Pastry, 5th Intl. Conf. Abstract State Machines, p.2016, 2016.
DOI : 10.1007/978-3-319-33600-8_5

URL : https://hal.archives-ouvertes.fr/hal-01322342

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA???+??? Proofs, 18th Intl. Symp. Formal Methods, pp.147-154, 2012.
DOI : 10.1007/978-3-642-32759-9_14

URL : https://hal.archives-ouvertes.fr/hal-00726632

H. Kopetz and G. Bauer, The time-triggered architecture, Proc. of the IEEE, pp.112-126, 2003.

L. Lamport, Specifying Systems, 2002.

L. Lamport, Byzantizing Paxos by Refinement, 25th Intl. Symp. Distributed Algorithms (DISC 2011, pp.211-224, 2011.
DOI : 10.1007/978-3-642-03466-4_2

M. Lemerre, V. David, C. Aussagus, and G. Vidal-naquet, Equivalence between Schedule Representations: Theory and Applications, 2008 IEEE Real-Time and Embedded Technology and Applications Symposium, pp.237-247, 2008.
DOI : 10.1109/RTAS.2008.17

URL : https://hal.archives-ouvertes.fr/hal-00292628

M. Lemerre and E. Ohayon, A Model of Parallel Deterministic Real-Time Computation, 2012 IEEE 33rd Real-Time Systems Symposium, pp.273-282, 2012.
DOI : 10.1109/RTSS.2012.78

M. Lemerre, E. Ohayon, D. Chabrol, M. Jan, and M. Jacques, Method and Tools for Mixed-Criticality Real-Time Applications within PharOS, 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, pp.41-48, 2011.
DOI : 10.1109/ISORCW.2011.15

M. Leuschel and M. J. Butler, ProB: an automated analysis toolset for the B method. Software Tools for Technology Transfer, pp.185-203, 2008.

S. Louise, M. Lemerre, C. Aussagù, and V. David, The OASIS Kernel: A Framework for High Dependability Real-Time Systems, 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp.95-103, 2011.
DOI : 10.1109/HASE.2011.38

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How Amazon web services uses formal methods, Communications of the ACM, vol.58, issue.4, pp.66-73, 2015.
DOI : 10.1145/2699417

H. Pfeifer and F. W. Henke, Modular formal analysis of the central guardian in the Time-Triggered Architecture, Reliability Engineering & System Safety, vol.92, issue.11, pp.1538-1550, 2007.
DOI : 10.1016/j.ress.2006.10.006

J. Rushby, An Overview of Formal Verification for the Time-Triggered Architecture, Formal Techniques in Real-Time and Fault- Tolerant Systems, pp.83-105, 2002.
DOI : 10.1007/3-540-45739-9_7

Y. Yu, P. Manolios, and L. Lamport, Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of LNCS, pp.54-66, 1999.
DOI : 10.1007/3-540-48153-2_6