J. Abrial, The B Book -Assigning Programs to Meanings, 1996.

J. Abrial, Extending B without Changing it (for Developing Distributed Systems ), First B conference, Putting into Practice Methods and Tools for Information System Design, IRIN, pp.169-191, 1996.

J. R. Abrial and L. Mussat, Introducing dynamic constraints in B, 98: Recent Advances in the Development and Use of the B Method, pp.83-128, 1998.
DOI : 10.1007/BFb0053357

F. Ambert, F. Bouquet, S. Chemin, S. Guenaud, B. Legeard et al., BZ-testing tools: A tool-set for test generation from Z and B using constraint logic programming, Formal Approaches to Testing of Software (FATES'02), pp.105-120, 2002.

D. Bert and F. Cave, Construction of Finite Labelled Transition Systems from B Abstract Systems, Integrated Formal Methods, pp.235-254, 1945.
DOI : 10.1007/3-540-40911-4_14

D. Cansell, D. Méry, and S. Merz, Predicate Diagrams for the Verification of Reactive Systems, Integrated Formal Methods, pp.380-397, 1945.
DOI : 10.1007/3-540-40911-4_22
URL : https://hal.archives-ouvertes.fr/inria-00099125

D. Cansell, D. Méry, and S. Merz, Diagram Refinements for the Design of Reactive Systems, Journal of Universal Computer Science, vol.7, issue.2, 2001.

S. Graf and H. Sa¨?disa¨?di, Construction of abstract state graphs with PVS, Computer-Aided Verification (CAV'97), 1997.
DOI : 10.1007/3-540-63166-6_10

C. A. Hoare, Communicating Sequential Processes, 1985.

L. 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

H. Ledang and J. Souquì-eres, Contributions for Modelling UML State-Charts in B, IFM, LNCS 2335, pp.109-127, 2002.
DOI : 10.1007/3-540-47884-1_7
URL : https://hal.archives-ouvertes.fr/inria-00099403

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

R. Marlet, DEMONEY: Java Card Implementation. Public technical report, SEC- SAFE project, 2002.

R. Marlet and C. Mesnil, DEMONEY : A demonstrative Electronic Purse -Card Specification -. Public technical report, SECSAFE project, 2002.

P. Samarati, S. De-capitani, and D. Vimercati, Access Control: Policies, Models, and Mechanisms. In Revised versions of lectures given during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design on Foundations of Security Analysis and Design, pp.137-196, 2001.

F. B. Schneider, Enforceable security policies. Information and System Security, pp.30-50, 2000.
DOI : 10.1109/fits.2003.1264930
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.147.1853

. Secsafe, SecSafe Porject Home Page

E. Sekerinski and R. Zurob, Translating Statecharts to B, IFM, LNCS 2335 21. SUN. Java Card, pp.128-144, 2002.
DOI : 10.1007/3-540-47884-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.94.2394

K. Trentelman and M. Huisman, Extending JML Specifications with Temporal Logic, Algebraic Methodology And Software Technology (AMAST '02), pp.334-348, 2002.
DOI : 10.1007/3-540-45719-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.6993

J. Voisinet and B. Tatibouet, Generating Statecharts from B Specifications, 16th Int Conf. on Software and System Engineering and their applications, 2003.