. Bibliographie and L. Abadi, Abadi and Lamport. The existence of refinement mappings, LICS : IEEE Symposium on Logic in Computer Science, 1988.

L. Abadi, L. Abadi, and . Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.507-534, 1995.
DOI : 10.1145/203095.201069

URL : http://www.research.digital.com/SRC/personal/lamport/pubs/abadi-composing.ps.Z

H. Abrial, Jean-Raymond Abrial and Stefan Hallerstede. Decomposition, refinement and instantiation of generic models, ASM 05, 2005.

H. Abrial, S. Abrial, and . Hallerstede, Refinement, decomposition , and instantiation of discrete models : Application to Event-B, 2006.

M. Abrial, L. Abrial, and . Mussat, Introducing dynamic constraints in B, The 2nd International B Conference, pp.83-128, 1998.
DOI : 10.1007/BFb0053357

. Abrial, Specification language, On the Construction of Programs : An Advanced Course, pp.343-410, 1980.

1. Abrial and . Abrial, The B-Book : Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

1. Abrial and . Abrial, Extending B without changing it (for developing distributed systems ), Proceedings of the 1st Conference on the B method, pp.169-191, 1996.

]. Abrial, Guidelines to formal system studies, MATISSE project, 2000.

]. Abrial, B#: Toward a Synthesis between Z and B, ZB'2003 ? Formal Specification and Development in Z and B, pp.168-177, 2003.
DOI : 10.1007/3-540-44880-2_12

K. J. Antsaklis, X. D. Antsaklis, and . Koutsoukos, Hybrid Systems: Review and Recent Progress, Chapter in Software- Enabled Control : Information Technologies for Dynamical Systems, 2003.
DOI : 10.1002/047172288X.ch14

. A. Arnold and . Arnold, An example of use of MEC : Verification of tromp's algorithm, 1992.

K. Back and K. Back, Stepwise refinement of action systems, Mathematics of Program Construction, pp.115-138, 1989.
DOI : 10.1007/3-540-51305-1_7

K. Back and K. Back, Stepwise refinement of action systems, Mathematics of Program Construction, pp.115-138, 1989.
DOI : 10.1007/3-540-51305-1_7

K. Back, R. Back, and . Kurki-suonio, Decentralization of process nets with centralized control, PODC, pp.131-142, 1983.

V. Back, . Wright-]-r-j, J. V. Back, and . Wright, Refinement Calculus : A Systematic Introduction. Graduate Texts in Computer Science, 1998.
DOI : 10.1007/978-1-4612-1674-2

V. Back, . Back, and W. Joakim-von, Refinement Calculus : A Systematic Introduction. Graduate Texts in Computer Science, 1998.
DOI : 10.1007/978-1-4612-1674-2

]. R. Back, On the correctness of refinement in program development, 1978.

B. Barradas, D. Barradas, and . Bert, Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems, 2002.
DOI : 10.1007/3-540-47884-1_20

B. Barradas, D. Barradas, and . Bert, Proof obligations for specification and refinement of liveness properties under weak fairness, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00004181

. Behm, M??t??or: A Successful Application of B in a Large Project, FM 99 ? World Conference on Formal Methods in the Development of Computing Systems, number 1708 in LNCS, pp.369-387, 1999.
DOI : 10.1007/3-540-48119-2_22

. Bellegarde, Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants, Lecture Notes in Computer Science, vol.1878, pp.230-245, 2000.
DOI : 10.1007/3-540-44525-0_14

. Bellegarde, Ready-Simulation Is Not Ready to Express a Modular Refinement Relation, Lecture Notes in Computer Science, vol.1783, pp.266-283, 2000.
DOI : 10.1007/3-540-46428-X_19

. Bellegarde, Reformulation: a Way to Combine Dynamic Properties and B Refinement, Lecture Notes in Computer Science, vol.2021, pp.2-19, 2001.
DOI : 10.1007/3-540-45251-6_2

. Bellegarde, Synchronized Parallel Composition of Event Systems in B, Lecture Notes in Computer Science, vol.2272, pp.436-457, 2002.
DOI : 10.1007/3-540-45648-1_23

. Benveniste, Synchronous programming with events and relations: the SIGNAL language and its semantics, Science of Computer Programming, vol.16, issue.2, pp.103-149, 1991.
DOI : 10.1016/0167-6423(91)90001-E

C. Berry, L. Berry, . Cosseratberry, G. Gonthier, G. Berry et al., The esterel synchronous programming language and its mathematical semantics The ESTEREL synchronous programming language : design, semantics, implementation, Proceedings of the Seminar on Concurrency, pp.389-44887, 1984.

. Berry, Esterel : Towards a synchronous and semantically sound high level language for real-time applications, Proceedings of the 1983 IEEE Real-Time Systems Symposium

]. G. Berry, The Foundations of Esterel, 2000.

J. Bjorner, C. B. Bjorner, and . Jones, The vienna development method : the meta-language. In The vienna development method : the meta-language, Lecture Notes in Computer Science, 1978.

. Blass, Interactive smallstep algorithms 2 : abstract state machines and the characterization theorem. To appear in Logical methods in Computer Science A preliminary version appeared as Microsoft resarch report MSR-TR, 2006.
DOI : 10.2168/lmcs-3(4:4)2007

URL : https://lmcs.episciences.org/1201/pdf

. Bodeveix, A formalization of the B method in Coq and PVS, FM'99 ? B Users Group Meeting ? Applying B in an industrial context : Tools, Lessons and Techniques, pp.32-48, 1999.

. Bodeveix, Jean-Paul Bodeveix, Mamoun Filali, and Miloud Rached. Méthodes de spécification de systèmes temps réel en B, 2004.

. Bozga, Kronos : A model-checking tool for real-time systems, Proc. 10th International Computer Aided Verification Conference, pp.546-550, 1998.
DOI : 10.1007/bfb0028779

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

R. Broadfoot, J. Philippa, A. W. Broadfoot, and . Roscoe, Tutorial on FDR and Its Applications, Lecture Notes in Computer Science, vol.1885, p.322, 2000.
DOI : 10.1007/10722468_18

J. Michael and . Butler, Stepwise refinement of communicating systems, Science of Computer Programming, vol.27, issue.2, pp.139-173, 1996.

J. Michael and . Butler, csp2B : A practical approach to combining CSP and B. Formal Asp, Comput, vol.12, issue.3, pp.182-198, 2000.

. Cansell, Diagram refinements for the design of reactive systems, Journal of Universal Computer Science, vol.7, issue.2, pp.159-174, 2001.

. Cansell, Formal analysis of a self-stabilizing algorithm using predicate diagrams, Workshop Integrating Diagrammatic and Formal Specification Techniques, pp.39-45, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00110548

. Caspi, Lustre : A declarative language for programming synchronous systems, POPL, pp.178-188, 1987.
DOI : 10.1145/41625.41641

M. M. Chandy, J. Chandy, and . Misra, Parallel Program Design, 1988.
DOI : 10.1007/978-1-4613-9668-0_6

]. A. Chombart, Commande supervisée des systèmes hybrides, Thèse de doctorat. Institut Nationale Polytechnique de, 1997.

. Clarke, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

. Clearsy, Atelier b. Technical Note Version 3, 2002.

. Clearsy, Atelier b. Technical Note Version 3, 2002.

S. De-groote, . Ph, S. De-groote, and . Salvati, Higher-Order Matching in the Linear ??-calculus with Pairing, Lecture Notes in Computer Science, vol.3210, pp.220-234, 2004.
DOI : 10.1007/978-3-540-30124-0_19

URL : https://hal.archives-ouvertes.fr/inria-00100082

G. De, Ph. de Groote. Partially commutative linear logic : sequence calculus and phase semantics, Proofs and linguitic categories, 1996.
URL : https://hal.archives-ouvertes.fr/hal-00145752

]. Dijkstra, A discipline of programming, 1976.

. Fejoz, DIXIT : a graphical toolkit for predicate abstractions, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000767

]. Fowler, ANALYSIS PATTERNS, 1997.
DOI : 10.1017/CBO9780511550881.013

S. Bowen, M. King, and . Waldén, ZB'2003 ? Formal Specification and Development in Z and B, volume 2651 of, Lecture Notes in Computer Science, pp.101-102, 2003.

. Hammer, Truly On-the-Fly LTL Model Checking, 2005.
DOI : 10.1007/978-3-540-31980-1_13

URL : https://hal.archives-ouvertes.fr/inria-00000753

]. D. Harel, STATEMATE : a working environment for the development of complex reactive systems, Proc 10th IEEE Conf on Software Engineering, 1988.

. Harel, On the formal semantics of statecharts, LICS : IEEE Symposium on Logic in Computer Science, 1987.

. Henzinger, HyTech: A model checker for hybrid systems, Lecture Notes in Computer Science, vol.1254, pp.460-463, 1997.
DOI : 10.1007/3-540-63166-6_48

URL : http://www.cis.upenn.edu/~lee/99cis642/papers/hytech.ps

]. C. Hoare, J. Gerald, and . Holzmann, Communicating Sequential Processes Series in Computer Science The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1985.

J. Gerard and . Holzmann, The SPIN Model Checker, 2003.

. C. Jones and . Jones, Development Methods for Computer Programmes Including a Notion of Interference, Prgr.Res.Grp, vol.25

. Julliand, Modular Verification of Dynamic Properties for Reactive Systems, In IFM, pp.89-108, 1999.
DOI : 10.1007/978-1-4471-0851-1_6

[. Chandy, J. Misra-]-k-m, J. Chandy, and . Misra, Parallel Program Design, 1989.
DOI : 10.1007/978-1-4613-9668-0_6

V. Kupferman, M. Y. Kupferman, and . Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems, vol.22, issue.1, pp.87-128, 2000.
DOI : 10.1145/345099.345104

]. L. Lamport, The temporal logic of actions, Digital Equipment Corporation, Systems Research Centre, 1991.
DOI : 10.1145/177492.177726

. L. Lamport and . Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

L. Lamport and . Lamport, Introduction to TLA, 1994.

]. Lamport, Refinement in state-based formalisms, 1996.

]. L. Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

H. Lano, H. Lano, and . Haughton, Specification in B : An Introduction Using the B Toolkit, 1996.
DOI : 10.1142/p006

. Lano, Using B to design and verify controllers for chemical processing, Proceedingsof 1st Conference on the B method, pp.237-270, 1996.

. Lano, Extending B AMN with concurrency, 1996.

. Lano, Extending B AMN with concurrency, Dept. of Computing, 1996.

]. K. Lano, The B Language and Method : A guide to Practical Formal Development, 1996.
DOI : 10.1007/978-1-4471-1494-9

. Larsen, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.
DOI : 10.1007/s100090050010

. Larsen, Uppaal: Status & developments, Lecture Notes in Computer Science, vol.1254, pp.456-459, 1997.
DOI : 10.1007/3-540-63166-6_47

URL : http://www.docs.uu.se/docs/rtmv/papers/lpw:cav97.ps.gz

G. Leduc, F. Leduc, and . Germeau, Verification of security protocols using LOTOS-method and application, Computer communications Special issue on formal description techniques in practice, pp.1089-1103, 2000.
DOI : 10.1016/S0140-3664(99)00239-X

B. Leuschel and M. Butler, ProB: A Model Checker for B, FME 2003 : Formal Methods, LNCS 2805, pp.855-874, 2003.
DOI : 10.1007/978-3-540-45236-2_46

B. Leuschel and M. Butler, ProB: A Model Checker for B, FME 2003 : Formal Methods, LNCS 2805, pp.855-874, 2003.
DOI : 10.1007/978-3-540-45236-2_46

]. R. Lewis, Modelling control systems using iec 61499, Institution Of Engineering and Technology (UK), 2001.

D. Méry, A proof system to derive evantually properties under justice hypothesis, MFCS, pp.536-544, 1986.

D. Méry, Méthode axiomatique pour les propriétés de fatalité des programmes parallèles, ITA, vol.21, issue.3, pp.287-322, 1987.

]. S. Merz, An encoding of TLA in isabelle, 1999.

S. Merz, Model Checking: A Tutorial Overview, Modeling and Verification of Parallel Processes, pp.3-38, 2001.
DOI : 10.1007/3-540-45510-8_1

URL : http://www.loria.fr/~merz/papers/mc-tutorial.pdf

S. Merz, Model Checking Techniqes for the Analysis of Reactive Systems, Synthese, vol.133, issue.1/2, pp.173-201, 2002.
DOI : 10.1023/A:1020887910943

S. Merz, On the logic of tla +, Computers and Informatics, vol.22, pp.351-379, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099800

]. Morgan, Programming from Specifications : Second Edition, 1994.

M. Joseph and . Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, vol.9, issue.3, pp.287-306, 1987.

. Mosbahi, . O. Jaray, J. Mosbahi, and . Jaray, Représentation du temps en b événementiel pour la modélisation des systèmes temps réel, 2004.

. Mosbahi, . O. Jaray, J. Mosbahi, and . Jaray, Une démarche formelle de développement de systèmes de contrôle-commande, 2004.

J. Mosbahi, J. Mosbahi, and . Jaray, Specification and proof of liveness properties in b event systems, ICSOFT. 2th International Conference on Software and Data Technology, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00158906

J. Mosbahi, L. Mosbahi, and . Jemni, Utilisation conjointe de la méthode b événementiel et de la logique temporelle tla+ pour la modélisation et la vérification des systèmes réactifs, MOSIM, Modélisation, Optimisation et Simulation des Systèmes, 2006.

. Mosbahi, A formal development approach of control systems using the event based b approch, case study : A parcel sorting device, ACS/IEEE, International Conference on Computer Systems and Applications, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000801

. Mosbahi, A formal development approach of automated systems using the temporal logic of actions tla+, MOSIM, Modélisation, Optimisation et Simulation des Systèmes, 2006.

. Mosbahi, Spécification et vérification des propriétés de vivacité en b événementiel, MSR. Modélisation des systèmes réactifs, 2007.

. Mosbahi, A formal approach of the development of automated systems, ICSOFT. 2th International Conference on Software and Data Technology, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00158908

. Mountassir, Coopération entre preuve et model-checking pour vérifier modulairement des propriétés LTL, AFADL'2000, pp.127-141, 2000.

. Murata, Petri-net model and minimum cycle time for updating moving objects database, ] Tobias Nipkow. Isabelle HOL -the tutorialNise, 2003] N. S. Nise. Control systems engineering. WileyOstroff, 1989] J. Ostroff. Temporal Logic for Real-Time Systems. Advanced Software Development Series, pp.211-217, 1989.

. Owre, PVS: A prototype verification system, 11th International Conference on Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

URL : http://www.csl.sri.com/papers/c/a/cade92-pvs/cade92-pvs.ps.gz

]. A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems, REX School-Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, 1988.

. Pnueli, System specification and refinement in temporal logic, FSTTCS : Foundations of Software Technology and Theoretical Computer Science, vol.12, 1992.
DOI : 10.1007/3-540-56287-7_92

]. Potet, Spécifications et développements formels : Etude des aspects compositionnels dans la méthode B, Thèse d'habilitation, LSR-IMAG, 2002.

P. Pouzancre, Mod??lisation en B ??v??nementiel des fonctions m??caniques, ??lectriques et informatiques d'un v??hicule, Techniques et sciences informatiques, vol.22, issue.1, pp.119-128, 2003.
DOI : 10.3166/tsi.22.119-128

]. Pouzancre, How to Diagnose a Modern Car with a Formal B Model?, ZB'2003 ? Formal Specification and Development in Z and B,International Conference of B and Z Users Proceedings, volume 2651 of Lecture Notes in Computer Science, pp.98-100, 2003.
DOI : 10.1007/3-540-44880-2_7

]. P. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM Journal on Control and Optimization, vol.25, issue.1, pp.206-230, 1987.
DOI : 10.1137/0325013

W. J. Ramadge, W. M. Ramadge, and . Wonham, The control of discrete event systems, Proceedings of the IEEE, vol.77, issue.1, pp.81-98, 1989.
DOI : 10.1109/5.21072

]. A. Roscoe, The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science, 1998.

]. J. Rushby, Theorem Proving for Verification, Proceedings of Summer School of Modelling and Verification of Parallel Processes, pp.39-57, 2000.
DOI : 10.1007/3-540-45510-8_2

URL : http://www.csl.sri.com/users/rushby/papers/movep2k.ps.gz

H. Treharne, Communicating B machines, Lecture Notes in Computer Science, vol.2272, pp.416-435, 2002.

. J. Shoenfield and . Shoenfield, Axoims of set theory, hnbk, chapter, pp.321-344, 1978.

]. J. Spivey, The Z Notation. A Reference Manual, 1992.

. Treharne, Composing Specifications Using Communication, ZB'2003 ? Formal Specification and Development in Z and B,International Conference of B and Z Users Proceedings, volume 2651 of Lecture Notes in Computer Science, pp.58-78, 2003.
DOI : 10.1007/3-540-44880-2_5

URL : http://www.cs.rhul.ac.uk/~helen/papers/zb2003/treharne_2003.ps

W. Peter, Concurrent systems, CSP, and FDR, 2002.

M. Zhang, A. K. Zhang, and . Mackworth, Synthesis of hybrid constraint-based controllers, Lecture Notes in Computer Science, vol.999, pp.552-567, 1995.
DOI : 10.1007/3-540-60472-3_28