. A. Abj-+-99-]-p, A. Abdulla, B. Bouajjani, M. Jonsson, . R. Nilssonabr05-]-j et al., Handling Global Conditions in Parameterized System Verification The B-Book -Assigning programs to meanings Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems, Proceedings of CAVAbr10] J.R. Abrial. Modeling in Event-B: System and Software Engineering Proceedings of Integrated Formal Methods, pp.134-145, 1999.

]. A. Bcc-+-99, A. Biere, E. Cimatti, Y. Clarke, . [. Zhu et al., Symbolic Model Checking without BDDs Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions Handbook of Process Algebra, Analysis of Systems ZB 2002:Formal Specification and Development in Z and B Algebra of Communicating Processes with Abstraction. TCS, pp.193-207, 1985.

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An opensource tool for symbolic model checking Automatic verification of finite-state concurrent systems using temporal logic specifications, EL + 86] E. A. Emerson and C-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus Proceedings of Logic in Computer Science, pp.244-263, 1986.

H. Evans, R. Treharne, M. Laleau, M. Frappier, B. Frappier et al., How to verify dynamic properties of information systems Comparison of model checking tools for information systems, Workshop of Software Engineering and Formal Methods Proceedings of ICFEMFdr97] Formal Systems (Europe) Ltd. Failures-Divergences Refinement. FDR2 User Manual, pp.416-425, 1997.

M. Frappier, R. St, and . Denis, eb 3 : an entity-based black-box specification method for information systems, Journal of Software and System Modeling, pp.134-149, 2003.

H. Garavel, F. Lang, R. Mateescu, W. Serweger06-]-f, and . Gervais, CADP 2010: A toolbox for the construction and analysis of distributed processes Combinaison de spécifications formelles pour la modélisation des systèmes d'information, Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, pp.372-387, 2006.

F. Gervais, M. Frappier, and R. Laleau, Synthesizing B Specifications from eb 3 Attribute Definitions, Proceedings of Integrated Formal Methods, pp.207-226, 2005.
DOI : 10.1007/11589976_13
URL : https://hal.archives-ouvertes.fr/hal-01125054

F. Gervais, M. Frappier, R. A. Laleauhoa78-]-c, . Hoareha11-]-t-s, J. Hoang et al., Refinement of eb 3 Process Patterns into B Specifications Communicating Sequential Processes Reasoning about liveness properties in Event-B The Spin Model Checker: Primer and Reference Manual, Proceedings of Formal Specification and Development in B, LNCS Proceedings of Formal Engineering MethodsJac06] D. Jackson. Software Abstractions, pp.201-215, 1978.

. E. Jfg-+-10-]-m, M. Jiague, F. Frappier, P. Gervais, R. Konopacki et al., Model-Driven Engineering of Functional Security Policies Enhancements to LOTOS (E-LOTOS) International Standard number 15437:2001, International Organization for Standardization ? Information Technology ProB: A model checker for B: How to make FDR spin: LTL model checking of CSP by refinement, Proceedings of International Conference on Enterprise Information Proceedings of Symposium on Formal MethodsKoz83] D. Kozen. Results on the Propositional µ-calculus. In TCSMF15] A. Mammar, M. Frappier. Proof-based verification approaches for dynamic properties: application to the information system domain Journal of Formal Aspects of Computing, pp.374-379, 1983.

]. J. Mil-+-11, A. Milhau, R. Idani, M. A. Laleau, Y. Labiadh et al., Combining UML, ASTD and B for the formal specification of an access control filter A model checking language for concurrent value-passing systems, Proceedings of Formal Methods, pp.303-313, 2008.

D. Vekris, F. Lang, C. Dima, R. Mateescu-[-pnu77, and ]. A. Pnueli, The temporal logic of programs, In Journal of Foundations of Computer Science, vol.18, pp.46-57, 1977.

[. Queille and J. Sifakis, Fairness and related properties in transition systems ? a temporal logic to deal with fairness, Journal of Acta Informatica, pp.195-220, 1983.
DOI : 10.1007/BF00265555

]. R. Str82 and . Streett, Propositional Dynamic Logic of Looping and Converse, Information and Control, pp.121-141, 1982.

H. [. Schneider and . Treharne, CSP theorems for communicating B machines, Journal of Formal Aspects of Computing, pp.390-422, 2005.
DOI : 10.1007/s00165-005-0076-7

]. S. Stw-+-14, H. Schneider, H. Treharne, D. M. Wehrheim, and . Williams, Managing LTL Properties in Event-B Refinement, Proceedings of Integrated Formal Methods, pp.221-237, 2014.

S. [. Treharne, M. Schneider, and . Bramble, Composing Specifications Using Communication, Proceedings of ZB, pp.55-78, 2003.
DOI : 10.1007/3-540-44880-2_5

D. Vekris and C. Dima, Efficient Operational Semantics for $$ EB ^3$$ for Verification of Temporal Properties, Proceedings of Fundamentals of Software Engineering, pp.133-149, 2013.
DOI : 10.1007/978-3-642-40213-5_9

]. D. Vld-+-13, F. Vekris, C. Lang, R. Dima, and . Mateescu, Verification of EB 3 Specifications using CADP, Proceedings of Integrated Formal Methods, pp.61-76, 2013.

A. Lnt, Code for the Simplified Library Management System We give the optimized LNT code for the simplified Library Management System, with 2 members, 1 book, and NbLoans set to 1