Abadi and Lamport. The existence of refinement mappings, LICS : IEEE Symposium on Logic in Computer Science, 1988. ,
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
Jean-Raymond Abrial and Stefan Hallerstede. Decomposition, refinement and instantiation of generic models, ASM 05, 2005. ,
Refinement, decomposition , and instantiation of discrete models : Application to Event-B, 2006. ,
Introducing dynamic constraints in B, The 2nd International B Conference, pp.83-128, 1998. ,
DOI : 10.1007/BFb0053357
Specification language, On the Construction of Programs : An Advanced Course, pp.343-410, 1980. ,
The B-Book : Assigning Programs to Meanings, 1996. ,
DOI : 10.1017/CBO9780511624162
Extending B without changing it (for developing distributed systems ), Proceedings of the 1st Conference on the B method, pp.169-191, 1996. ,
Guidelines to formal system studies, MATISSE project, 2000. ,
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
Hybrid Systems: Review and Recent Progress, Chapter in Software- Enabled Control : Information Technologies for Dynamical Systems, 2003. ,
DOI : 10.1002/047172288X.ch14
An example of use of MEC : Verification of tromp's algorithm, 1992. ,
Stepwise refinement of action systems, Mathematics of Program Construction, pp.115-138, 1989. ,
DOI : 10.1007/3-540-51305-1_7
Stepwise refinement of action systems, Mathematics of Program Construction, pp.115-138, 1989. ,
DOI : 10.1007/3-540-51305-1_7
Decentralization of process nets with centralized control, PODC, pp.131-142, 1983. ,
Refinement Calculus : A Systematic Introduction. Graduate Texts in Computer Science, 1998. ,
DOI : 10.1007/978-1-4612-1674-2
Refinement Calculus : A Systematic Introduction. Graduate Texts in Computer Science, 1998. ,
DOI : 10.1007/978-1-4612-1674-2
On the correctness of refinement in program development, 1978. ,
Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems, 2002. ,
DOI : 10.1007/3-540-47884-1_20
Proof obligations for specification and refinement of liveness properties under weak fairness, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-00004181
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
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
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
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
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
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
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. ,
Esterel : Towards a synchronous and semantically sound high level language for real-time applications, Proceedings of the 1983 IEEE Real-Time Systems Symposium ,
The Foundations of Esterel, 2000. ,
The vienna development method : the meta-language. In The vienna development method : the meta-language, Lecture Notes in Computer Science, 1978. ,
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
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. ,
Jean-Paul Bodeveix, Mamoun Filali, and Miloud Rached. Méthodes de spécification de systèmes temps réel en B, 2004. ,
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
Tutorial on FDR and Its Applications, Lecture Notes in Computer Science, vol.1885, p.322, 2000. ,
DOI : 10.1007/10722468_18
Stepwise refinement of communicating systems, Science of Computer Programming, vol.27, issue.2, pp.139-173, 1996. ,
csp2B : A practical approach to combining CSP and B. Formal Asp, Comput, vol.12, issue.3, pp.182-198, 2000. ,
Diagram refinements for the design of reactive systems, Journal of Universal Computer Science, vol.7, issue.2, pp.159-174, 2001. ,
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
Lustre : A declarative language for programming synchronous systems, POPL, pp.178-188, 1987. ,
DOI : 10.1145/41625.41641
Parallel Program Design, 1988. ,
DOI : 10.1007/978-1-4613-9668-0_6
Commande supervisée des systèmes hybrides, Thèse de doctorat. Institut Nationale Polytechnique de, 1997. ,
Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994. ,
DOI : 10.1145/186025.186051
Atelier b. Technical Note Version 3, 2002. ,
Atelier b. Technical Note Version 3, 2002. ,
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
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
A discipline of programming, 1976. ,
DIXIT : a graphical toolkit for predicate abstractions, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00000767
ANALYSIS PATTERNS, 1997. ,
DOI : 10.1017/CBO9780511550881.013
ZB'2003 ? Formal Specification and Development in Z and B, volume 2651 of, Lecture Notes in Computer Science, pp.101-102, 2003. ,
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
STATEMATE : a working environment for the development of complex reactive systems, Proc 10th IEEE Conf on Software Engineering, 1988. ,
On the formal semantics of statecharts, LICS : IEEE Symposium on Logic in Computer Science, 1987. ,
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
Communicating Sequential Processes Series in Computer Science The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1985. ,
The SPIN Model Checker, 2003. ,
Development Methods for Computer Programmes Including a Notion of Interference, Prgr.Res.Grp, vol.25 ,
Modular Verification of Dynamic Properties for Reactive Systems, In IFM, pp.89-108, 1999. ,
DOI : 10.1007/978-1-4471-0851-1_6
Parallel Program Design, 1989. ,
DOI : 10.1007/978-1-4613-9668-0_6
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
The temporal logic of actions, Digital Equipment Corporation, Systems Research Centre, 1991. ,
DOI : 10.1145/177492.177726
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
Introduction to TLA, 1994. ,
Refinement in state-based formalisms, 1996. ,
Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, 2002. ,
Specification in B : An Introduction Using the B Toolkit, 1996. ,
DOI : 10.1142/p006
Using B to design and verify controllers for chemical processing, Proceedingsof 1st Conference on the B method, pp.237-270, 1996. ,
Extending B AMN with concurrency, 1996. ,
Extending B AMN with concurrency, Dept. of Computing, 1996. ,
The B Language and Method : A guide to Practical Formal Development, 1996. ,
DOI : 10.1007/978-1-4471-1494-9
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
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
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
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
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
Modelling control systems using iec 61499, Institution Of Engineering and Technology (UK), 2001. ,
A proof system to derive evantually properties under justice hypothesis, MFCS, pp.536-544, 1986. ,
Méthode axiomatique pour les propriétés de fatalité des programmes parallèles, ITA, vol.21, issue.3, pp.287-322, 1987. ,
An encoding of TLA in isabelle, 1999. ,
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
Model Checking Techniqes for the Analysis of Reactive Systems, Synthese, vol.133, issue.1/2, pp.173-201, 2002. ,
DOI : 10.1023/A:1020887910943
On the logic of tla +, Computers and Informatics, vol.22, pp.351-379, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099800
Programming from Specifications : Second Edition, 1994. ,
A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, vol.9, issue.3, pp.287-306, 1987. ,
Représentation du temps en b événementiel pour la modélisation des systèmes temps réel, 2004. ,
Une démarche formelle de développement de systèmes de contrôle-commande, 2004. ,
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
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. ,
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
A formal development approach of automated systems using the temporal logic of actions tla+, MOSIM, Modélisation, Optimisation et Simulation des Systèmes, 2006. ,
Spécification et vérification des propriétés de vivacité en b événementiel, MSR. Modélisation des systèmes réactifs, 2007. ,
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
Coopération entre preuve et model-checking pour vérifier modulairement des propriétés LTL, AFADL'2000, pp.127-141, 2000. ,
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. ,
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
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. ,
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
Spécifications et développements formels : Etude des aspects compositionnels dans la méthode B, Thèse d'habilitation, LSR-IMAG, 2002. ,
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
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
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
The control of discrete event systems, Proceedings of the IEEE, vol.77, issue.1, pp.81-98, 1989. ,
DOI : 10.1109/5.21072
The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science, 1998. ,
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
Communicating B machines, Lecture Notes in Computer Science, vol.2272, pp.416-435, 2002. ,
Axoims of set theory, hnbk, chapter, pp.321-344, 1978. ,
The Z Notation. A Reference Manual, 1992. ,
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
Concurrent systems, CSP, and FDR, 2002. ,
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