M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Conference Record of POPL 2001 : The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

J. , The B-book : Assigning Programs to Meanings, 1996.

J. Abrial, Modeling in Event-B : System and Software Engineering, 2010.

J. Abrial, M. Butler, S. Hallerstede, S. Thai, F. Hoang et al., Rodin : an open toolset for modelling and reasoning in Event-B, International journal on software tools for technology transfer, vol.12, issue.6, pp.447-466, 2010.

J. Abrial, M. Butler, S. Hallerstede, and M. Leuschel, Matthias Schmalz, and Laurent Voisin. Proposals for mathematical extensions for Event-B, 2009.

J. Abrial, M. J. Butler, S. Hallerstede, and L. Voisin, A roadmap for the rodin toolset, ABZ, vol.5238, p.347, 2008.

J. Abrial and S. Hallerstede, Refinement, decomposition, and instantiation of discrete models : Application to Event-B. Fundamenta Informaticae, vol.77, pp.1-28, 2007.

J. Abrial and T. Hoang, Using design patterns in formal methods : An Event-B approach, Lecture Notes in Computer Science, vol.5160, pp.1-2, 2008.

Y. Ait-ameur and D. Méry, Making explicit domain knowledge in formal system development, Science of Computer Programming, vol.121, pp.100-127, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01245832

A. Akerman and J. Tyree, Using ontology to support development of software architectures, IBM Systems Journal, vol.45, issue.4, pp.813-826, 2006.

V. Akman and M. Surav, The use of situation theory in context modeling, Computational Intelligence, vol.13, issue.3, pp.427-438, 1997.

H. Eman and . Alkhammash, Derivation of Event-B Models from OWL Ontologies, MATEC Web of Conferences, vol.76, p.4008, 2016.

P. Alpar and S. Olbrich, Legal requirements and modelling of processes in e-government, Electronic journal of e-government, vol.3, issue.3, pp.107-116, 2005.

Y. Aït-ameur, J. P. Gibson, and D. Méry, On Implicit and Explicit Semantics : Integration Issues in Proof-Based Development of Systems, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications -6th International Symposium, vol.8803, pp.604-618, 2014.

R. Anane, R. Freeland, and G. K. Theodoropoulos, e-voting requirements and implementation, 9th IEEE International Conference on E-Commerce Technology (CEC 2007) / 4th IEEE International Conference on Enterprise Computing, E-Commerce and E-Services, pp.382-392, 2007.

M. Bruno and A. , Développement d'algorithmes répartis corrects par construction. (Developing correct-by-construction distributed algorithms), 2015.

M. Bruno-andriamiarina, D. Méry, and N. Singh, Integrating proved state-based models for constructing correct distributed algorithms, Johnsen and Petre, vol.158, pp.268-284

, Aristote. Oeuvres complètes. Flammarion, 2014.

A. Arnaud, Recension de Jean-Louis Le Moigne, La modélisation des systèmes complexes, vol.19, pp.424-424, 1990.

A. Arnold, Systèmes de transitions finis et sémantique des processus communicants. Etudes et recherches en informatique, 1992.

A. Artale and E. Franconi, A temporal description logic for reasoning about actions and plans, J. Artif. Intell. Res, vol.9, pp.463-506, 1998.

C. Artho, D. Drusinksy, A. Goldberg, K. Havelund, M. Lowry et al., Experiments with test case generation and runtime analysis, Proceedings of the Abstract State Machines 10th International Conference on Advances in Theory and Practice, ASM'03, pp.87-108, 2003.

N. Aussenac-gilles, Bottom-up methods for Knowledge Engineering. Habilitation à diriger des recherches, 2005.
URL : https://hal.archives-ouvertes.fr/tel-00089165

F. Baader, The description logic handbook : theory, implementation, and applications, 2003.

F. Baader, D. Calvanese, D. L. Mcguinness, and D. Nardi, The Description Logic Handbook : Theory, Implementation, and Applications, 2003.

R. Back and M. Butler, Fusion and simultaneous execution in the refinement calculus, Acta Informatica, vol.35, issue.11, pp.921-949, 1998.

M. Backes, C. Hritcu, and M. Maffei, Automated verification of remote electronic voting protocols in the applied pi-calculus, Proceedings of the 21st IEEE Computer Security Foundations Symposium, pp.195-209, 2008.

P. Barlatier, Conception et implantation d'un modèle de raisonnement sur les contextes basé sur une théorie des types et utilisant une ontologie de domaine, 2009.

J. Barwise, Conditionals and conditional information, On Conditionals, pp.21-54, 1986.

J. Barwise, The situation in logic, Number 17. Center for the Study of Language (CSLI), 1989.

J. Barwise and J. Perry, Situations and Attitudes, 1983.

A. Baskar, R. Ramanujam, and S. P. Suresh, Knowledge-based modelling of voting protocols, Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge, TARK '07, pp.62-71, 2007.

N. Benaïssa, Modelling Attacker's Knowledge for Cascade Cryptographic Protocols, First International Conference on Abstract State Machines, B and Z -ABZ 2008, vol.5238, pp.251-264, 2008.

N. Benaïssa, La composition des protocoles de sécurité avec la méthode B évé-nementielle. (Security protocols composition using Event B), 2010.

N. Benaïssa and D. Méry, Cryptographic protocols analysis in event B, Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, vol.5947, pp.282-293, 2009.

N. Benaïssa and D. Méry, Proof-based design of security protocols, Computer Science -Theory and Applications, 5th International Computer Science Symposium in Russia, CSR 2010, vol.6072, pp.25-36, 2010.

J. Benaloh and D. Tuinstra, Receipt-free secret-ballot elections (extended abstract), Proceedings of the Twenty-sixth Annual ACM Symposium on Theory of Computing, STOC '94, pp.544-553, 1994.

J. Bendisposto and M. Leuschel, Proof assisted model checking for B, Proceedings of ICFEM 2009, vol.5885, pp.504-520, 2009.

B. Bérard and M. Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and software verification : model-checking techniques and tools, 2013.

Y. Beresnevichiene, A role and context based security model, 2003.

M. A. Bishop, The Art and Science of Computer Security, 2002.

D. Bjørner, Rôle of domain engineering in software development -why current requirements engineering is flawed ! In Ershov Memorial Conference, Lecture Notes in Computer Science, vol.5947, pp.2-34, 2009.

D. Bjørner, From Domains to Requirements : A Gentle Introduction to Domain Engineering, Lecture Notes, 2012.

D. Bjørner, Manifest Domains : Analysis and Description, Lecture Notes, 2015.

D. Bjørner, Domain analysis & description -the implicit and explicit semantics problem, Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), IMPEX/FM&MDD 2017, and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), vol.271, pp.1-23, 2017.

D. Bjørner and A. Eir, Compositionality : Ontology and mereology of domains, Concurrency, Compositionality, and Correctness, vol.5930, pp.22-59, 2010.

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, CSFW '01, pp.82-96, 2001.

B. Blanchet, M. Abadi, and C. Fournet, Automated verification of selected equivalences for security protocols, LICS, pp.331-340, 2005.

J. Paul-bodeveix, M. Filali, and C. A. Muñoz, A Formalization of the B-Method in Coq and PVS, LNCS, vol.1709, pp.33-49, 1999.

B. W. Boehm, Verifying and validating software requirements and design specifications, IEEE Softw, vol.1, issue.1, pp.75-88, 1984.

W. Barry and . Boehm, A spiral model of software development and enhancement, Computer, vol.21, issue.5, pp.61-72, 1988.

W. Bohlken, P. Koopmann, and B. Neumann, SCENIOR : Ontology-based Interpretation of Aircraft Service Activities, 2011.

P. Boldini, Formalizing context in intuitionistic type theory, Fundam. Inform, vol.42, issue.2, pp.105-127, 2000.

E. P. Bontas, D. Schlangen, and T. Schrader, Creating ontologies for content representation-the ontoseed suite, On the Move to Meaningful Internet Systems 2005 : CoopIS, DOA, and ODBASE, OTM Confederated International Conferences, CoopIS, DOA, and ODBASE 2005, vol.3761, pp.1296-1313, 2005.

A. Borgida, On the relative expressiveness of description logics and predicate logics, Artif. Intell, vol.82, issue.1-2, pp.353-367, 1996.

. Thouraya-(épouse, Tebibel) Bouabana. Une approche multi-formalismes pour la spécification et la vérification des systèmes communicants, 2007.

J. P. Bowen and M. G. Hinchey, Ten commandments of formal methods, Computer, vol.28, issue.4, pp.56-63, 1995.

J. Ronald, H. J. Brachman, and . Levesque, The tractability of subsumption in frame-based description languages, AAAI, pp.34-37, 1984.

D. Brade, A generalized process for the verification and validation of models and simulation results, 2004.

P. Brézillon, Context in problem solving : a survey, Knowledge Eng. Review, vol.14, issue.1, pp.47-80, 1999.

P. Brézillon, Hors du contexte, point de salut. Séminaire, Objets Communicants, vol.48, pp.74-90, 2002.

P. Brézillon and M. Cavalcanti, Modeling and using context, Knowledge Eng. Review, vol.13, issue.2, pp.185-194, 1998.

P. Brézillon and C. Tijus, Une representation basee sur le contexte des utilisateurs a travers leurs pratiques. Extraction et Gestion de Connaissances Paris, p.12, 2005.

J. Briffaut, Formalisation et garantie de propriétés de sécurité système : application à la détection d'intrusions. (Formalization and guaranty of system security properties : application to the detection of intrusions), 2007.

S. D. Brookes, C. A. Hoare, and A. W. Roscoe, A theory of communicating sequential processes, J. ACM, vol.31, issue.3, pp.560-599, 1984.

M. Butler, Decomposition structures for Event-B, Integrated Formal Methods, pp.20-38, 2009.
DOI : 10.1007/978-3-642-00255-7_2

URL : http://eprints.soton.ac.uk/266965/1/butler.pdf

M. J. Butler, csp2b : A practical approach to combining, CSP and B. Formal Asp. Comput, vol.12, issue.3, pp.182-198, 2000.
DOI : 10.1007/3-540-48119-2_28

URL : https://eprints.soton.ac.uk/253036/1/csp2b.pdf

S. Buvac, Quantificational logic of context, Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, AAAI 96, IAAI 96, vol.1, pp.600-606, 1996.

S. Buvac, V. Buvac, and I. A. Mason, Metamathematics of contexts. Fundam, Inform, vol.23, issue.2/3/4, pp.263-301, 1995.

C. Calero, F. Ruiz, and M. Piattini, Ontologies for Software Engineering and Software Technology, 2006.

V. Castañeda, L. Ballejos, M. L. Caliusco, and M. Galli, The use of ontologies in requirements engineering, Global Journal of Research In Engineering, vol.10, issue.6, 2010.

W. K. Samuel, J. Chan, and . Franklin, Dynamic context generation for natural language understanding : a multifaceted knowledge approach, IEEE Trans. Systems, Man, and Cybernetics, Part A, vol.33, issue.1, pp.23-41, 2003.

K. , M. Chandy, and J. Misra, Parallel program design -a foundation, 1989.

V. Chapurlat, Vérification et validation de modèles de systèmes complexes : application à la Modélisation d'Entreprise. Habilitation à diriger des recherches, 2007.

B. Chihani, E. Bertin, F. Jeanne, and N. Crespi, Context-aware systems : A case study, Digital Information and Communication Technology and Its Applications -International Conference, vol.167, pp.718-732, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00730472

A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., Nusmv 2 : An opensource tool for symbolic model checking, Computer Aided Verification, 14th International Conference, vol.2404, pp.359-364, 2002.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst, vol.8, issue.2, pp.244-263, 1986.

E. M. Clarke and E. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, Logic of Programs, Workshop, pp.52-71, 1982.

M. Clavel, F. Dur-Án, S. Eker, P. Lincoln, N. Mart-Í-oliet et al., Maude : specification and programming in rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.187-243, 2002.

, Election Assistance Commission. Voluntary Voting System Guidelines. Volume I : Version 1.0, United States, 2005.

V. Commission, European commission for democracy through law. Report on the Democratic Oversight of the Securiy Services. Adopted by the Venice Commission at its, vol.71, 2004.

R. Cooper, Records and record types in semantic theory, Journal of Logic and Computation, vol.15, issue.2, pp.99-112, 2005.

V. Cortier, G. Fuchsbauer, and D. Galindo, BeleniosRF : A strongly receipt-free electronic voting scheme, IACR Cryptology ePrint Archive, p.629, 2015.

V. Cortier, D. Galindo, S. Glondu, and M. Izabachène, A generic construction for voting correctness at minimum cost -application to helios, IACR Cryptology ePrint Archive, p.177, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00881079

V. Cortier, D. Galindo, S. Glondu, and M. Izabachene, Election verifiability for helios under weaker trust assumptions, Proceedings of the 19th European Symposium on Research in Computer Security (ESORICS'14), pp.327-344, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01011294

L. F. Cranor, Electronic voting : computerized polls may save money, protect privacy, Crossroads, vol.2, issue.4, pp.12-16, 1996.

L. F. Cranor and R. K. Cytron, Design and implementation of a practical security-conscious electronic polling system, 1996.

J. Crow and B. D. Vito, Formalizing space shuttle software requirements : Four case studies, ACM Trans. Softw. Eng. Methodol, vol.7, issue.3, pp.296-332, 0206.

J. L. Crowley, J. Coutaz, G. Rey, and P. Reignier, Perceptual components for context aware computing, UbiComp 2002 : Ubiquitous Computing, 4th International Conference, vol.2498, pp.117-134, 2002.

R. Aba-sah-dadzie, A. Bhagdev, S. Chakravarthy, J. Chapman, V. Iria et al., Applying semantic web technologies to knowledge sharing in aerospace engineering, J. Intelligent Manufacturing, vol.20, issue.5, pp.611-623, 2009.

K. Damchoom and M. Butler, Applying event and machine decomposition to a flash-based filestore in Event-B, Formal Methods : Foundations and Applications, pp.134-152, 2009.

R. Dapoigny and P. Barlatier, Modeling contexts with dependent types, Fundam. Inform, vol.104, issue.4, pp.293-327, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00547613

R. Davis, H. E. Shrobe, and P. Szolovits, What is a knowledge representation ? AI Magazine, vol.14, pp.17-33, 1993.

D. Déharbe, P. Fontaine, Y. Guyot, and L. Voisin, SMT solvers for rodin, Abstract State Machines, Alloy, B, VDM, and Z -Third International Conference, vol.7316, pp.194-207, 2012.

S. Delaune and S. Kremer, Spécificités des protocoles de vote électro-nique, Deliverable AVOTE, vol.1, issue.1, 2009.

S. Delaune, S. Kremer, and M. Ryan, Verifying privacy-type properties of electronic voting protocols, J. Comput. Secur, vol.17, issue.4, pp.435-487, 2009.

S. Delaune, S. Kremer, and M. D. Ryan, Coercion-resistance and receipt-freeness in electronic voting, Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.28-39, 2006.

G. Van-den-broeck, Lifted Inference and Learning in Statistical Relational Models (Eerste-orde inferentie en leren in statistische relationele modellen), 2013.

, The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004.

K. Devlin, Logic and information, 1991.

K. Anind and . Dey, Providing architectural support for building context-aware applications, 2000.

K. Anind and . Dey, Understanding and using context, Personal Ubiquitous Comput, vol.5, issue.1, pp.4-7, 2001.

P. Dhaussy and F. Boniol, Mise en oeuvre de composants MDA pour la validation formelle de modèles de systèmes d'information embarqués, Ingénierie des Systèmes d'Information, vol.12, issue.5, pp.133-157, 2007.

P. Dhaussy, F. Boniol, J. Roger, and L. Leroux, Improving model checking with context modelling, Adv. Software Engineering, vol.547157, issue.13, pp.1-547157, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00738735

P. Costa, J. P. Andrade-almeida, L. Ferreira-pires, G. Guizzardi, and M. J. Van-sinderen, Towards conceptual foundations for context-aware applications, AAAI Workshop on Modeling and Retrieval of Context 2006, volume WS-06-of AAAI Technical Report, pp.54-58, 2006.

D. Dolev and A. Yao, On the security of public key protocols, IEEE Trans. Information Theory, vol.29, issue.2, pp.198-207, 1983.

M. Dominique, Modèles et algorithmes, 2015.

F. M. Donini, M. Lenzerini, D. Nardi, and A. Schaerf, Deduction in concept languages : From subsumption to instance checking, J. Log. Comput, vol.4, issue.4, pp.423-452, 1994.

P. Dourish, Seeking a foundation for context-aware computing, Human-Computer Interaction, vol.16, issue.2-4, pp.229-241, 2001.

D. Drusinsky, The temporal rover and the atg rover, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pp.323-330, 2000.

A. Bruno-borlini-duarte, R. Luiz-de-castro-leal, . De-almeida, G. Falbo, R. S. Guizzardi et al., Ontological foundations for software requirements with a focus on requirements at runtime, Applied Ontology, vol.13, issue.2, pp.73-105, 2018.

S. Easterbrook, Verification and validation of requirements for mission critical systems, Proceedings of the 21st International Conference on Software Engineering, ICSE '99, pp.673-674, 1999.

E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg, -. Brckner et al., Casl : the common algebraic specification language, Theoretical Computer Science, vol.286, issue.2, pp.153-196, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00101008

H. Ehrig and B. Mahr, Equations und Initial Semantics, vol.1, 1985.

D. Ejigu, . Vasile-marian, L. Scuturici, and . Brunie, An ontology-based approach to context modeling and reasoning in pervasive computing, Fifth Annual IEEE International Conference on Pervasive Computing and Communications -Workshops (PerCom Workshops, pp.14-19, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00624654

J. Euzenat, J. Pierson, and F. Ramparany, Dynamic context management for pervasive applications, Knowledge Engineering Review, vol.23, issue.1, pp.21-49, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00793541

D. Fensel, Formal specification languages in knowledge and software engineering, Knowledge Eng. Review, vol.10, issue.4, pp.361-404, 1995.

S. Ferré, Systèmes d'information logiques : un paradigme logico-contextuel pour interroger, naviguer et apprendre, 2002.

D. Anthony-cw-finkelstein, A. Gabbay, J. Hunter, B. Kramer, and . Nuseibeh, Inconsistency handling in multiperspective specifications. Software Engineering, IEEE Transactions on, vol.20, issue.8, pp.569-578, 1994.

R. W. Floyd, Assigning meanings to programs, Mathematical Aspects of Computer Science, vol.19, pp.19-32, 1967.
DOI : 10.1007/978-94-011-1793-7_4

P. Fouque, Le partage de clés cryptographiques : Théorie et Pratique, 2001.

I. Nai-fovino and M. Masera, Through the description of attacks : A multidimensional view, Computer Safety, Reliability, and Security, 25th International Conference, vol.4166, pp.15-28, 2006.

F. K. Frantz, A taxonomy of model abstraction techniques, Proceedings of the 27th Conference on Winter Simulation, WSC '95, pp.1413-1420, 1995.

J. Fried, P. Gaudry, N. Heninger, and E. Thomé, A kilobit hidden SNFS discrete logarithm computation, EUROCRYPT (1), vol.10210, pp.202-231, 2017.
DOI : 10.1007/978-3-319-56620-7_8

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

A. Fujioka, T. Okamoto, and K. Ohta, A practical secret voting scheme for large scale elections, Advances in Cryptology -AUSCRYPT '92, Workshop on the Theory and Application of Cryptographic Techniques, vol.718, pp.244-251, 1992.
DOI : 10.1007/3-540-57220-1_66

B. Ganter and R. Wille, Formal concept analysis -mathematical foundations, 1999.

M. Gaudel, Structuring and modularizing algebraic specifications : The PLUSS specification language, evolutions and perspectives, STACS, vol.577, pp.3-18, 1992.
DOI : 10.1007/3-540-55210-3_169

J. , P. Gibson, S. Kherroubi, and D. Méry, Applying a Dependency Mechanism for Voting Protocol Models Using Event-B, Formal Techniques for Distributed Objects, Components, and Systems -37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, vol.10321, pp.124-138, 2017.
DOI : 10.1007/978-3-319-60225-7_9

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

J. , P. Gibson, and J. Raffy, Vote types : Generic modelling of functional requirements in impex projet, 2015.

F. Giunchiglia and C. Ghidini, Local models semantics, or contextual reasoning = locality + compatibility, Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), pp.282-291, 1998.

M. Glas, Ontology-based Model Integration for the Conceptual Design of Aircraft, 2013.

R. Godin, R. Missaoui, and A. , Experimental comparison of navigation in a galois lattice with conventional information retrieval methods, International Journal of Man-Machine Studies, vol.38, issue.5, pp.747-767, 1993.

C. P. Gomes, A. Sabharwal, and B. Selman, Model counting, Handbook of Satisfiability, vol.185, pp.633-654, 2009.

A. Gómez-pérez, Ontological engineering : A state of the art. Expert Update : Knowledge Based Systems and Applied Artificial Intelligence, vol.2, pp.33-43, 1999.

A. Gondal, M. Poppleton, and M. Butler, Composing Event-B specifications-case-study experience, Software Composition, pp.100-115
DOI : 10.1007/978-3-642-22045-6_7

URL : https://eprints.soton.ac.uk/271988/1/ICSCpaper.pdf

. Springer, , 2011.

M. J. Gordon and T. F. Melham, Introduction to HOL : A Theorem Proving Environment for Higher Order Logic, 1993.

Z. Graja, Vérification formelle des systèmes multi-agents auto-adaptatifs. (Formal verification of self-adaptive multi-agent systems), 2015.

, RAISE Language Group and Anne Elisabeth Haxthausen. The RAISE Specification Language, 1992.

R. Thomas and . Gruber, Toward principles for the design of ontologies used for knowledge sharing ? International journal of human-computer studies, vol.43, pp.907-928, 1995.

N. Guarino and C. Welty, Identity, unity, and individuality : Towards a formal toolkit for ontological analysis, Proceedings of the 14th European Conference on Artificial Intelligence, ECAI'00, pp.219-223, 2000.

N. Guarino and C. Welty, Identity and subsumption, The Semantics of Relationships, pp.111-126, 2002.

N. Guarino and C. A. Welty, A formal ontology of properties, Proceedings of the 12th European Workshop on Knowledge Acquisition, Modeling and Management, EKAW '00, pp.97-112, 2000.

G. Guizzardi and G. Guizzardi, Ontological foundations for structural conceptual models, vol.10, 2005.

G. Guizzardi and G. Wagner, Towards an ontological foundation of discrete event simulation, Proceedings of the 2010 Winter Simulation Conference, WSC 2010, pp.652-664, 2010.

C. Haskins, K. Forsberg, M. Krueger, D. Walden, and . Hamelin, Systems engineering handbook, INCOSE, 2006.

K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix et al., Formal analysis of the remote agent before and after flight, Proceedings of the 5th NASA Langley Formal Methods Workshop, vol.134, 2000.

S. Thai, J. Hoang, and . Abrial, Reasoning about liveness properties in Event-B, Formal Methods and Software Engineering -13th International Conference on Formal Engineering Methods, IC-FEM 2011, vol.6991, pp.456-471, 2011.

. Thai-son, A. Hoang, J. Fürst, and . Abrial, Event-B patterns and their tool support, Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM '09, pp.210-219, 2009.

. Thai-son, A. Hoang, J. Fürst, and . Abrial, Event-B patterns and their tool support. Software and System Modeling, vol.12, pp.229-244, 2013.

T. Hoang and J. Abrial, Event-b decomposition for parallel programs, Abstract State Machines, vol.5977, pp.319-333, 2010.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.

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

H. Hursti, EVEREST : Evaluation and Validation of Election-Related Equipment, Standards and Testing, 2007.

M. Jackson, Software Requirements &Amp ; Specifications : A Lexicon of Practice, Principles and Prejudices, 1995.

W. James, The will to believe and other essays. Longmans, Green, and Co, p.1897

M. Jarvisalo, D. L. Berre, O. Roussel, and L. Simon, The International SAT Solver Competitions, Artificial Intelligence Magazine (AI Magazine), vol.1, issue.33, pp.89-94, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00868244

S. Jean, OntoQL, un langage d'exploitation des bases de données à base ontologique. (OntoQL, an exploitation language for ontology-based databases), 2007.

, Integrated Formal Methods, 10th International Conference, IFM 2013, vol.7940, 2013.

C. B. Jones, Systematic Software Development Using VDM, 1990.

H. L. Jonker and W. Pieters, Receipt-freeness as a special case of anonymity in epistemic logic, Proc. Workshop On Trustworthy Elections (WOTE'06), 2006.

A. Juels, D. Catalano, and M. Jakobsson, Coercion-resistant electronic elections, Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, WPES '05, pp.61-70, 2005.

H. Kaiya and M. Saeki, Using domain ontology as domain knowledge for requirements elicitation, Proceedings of the 14th IEEE International Requirements Engineering Conference, RE '06, pp.186-195, 2006.

D. Kayser, La représentation des connaissances. Hermès, 1997.

S. Kherroubi, La contextualisation en Event-B, 2016.

S. Kherroubi and D. Méry, Contextualization and dependency in statebased modelling -application to Event-B, vol.207, pp.137-152
URL : https://hal.archives-ouvertes.fr/hal-01631017

M. Kifer, G. Lausen, and J. Wu, Logical foundations of object-oriented and frame-based languages, J. ACM, vol.42, issue.4, pp.741-843, 1995.

R. Klischewski, Semantic web for e-government, Roland Traunmüller, editor, Electronic Government, Second International Conference, vol.2739, pp.288-295, 2003.

A. Kofod-petersen and J. Cassens, Modeling and Retrieval of Context, Second International Workshop, MRC 2005, vol.3946, pp.1-17, 2005.

G. Kotonya and I. Sommerville, Requirements Engineering : Processes and Techniques, 1998.

S. Kremer and M. Ryan, Analysis of an electronic voting protocol in the applied pi calculus, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, vol.3444, pp.186-200, 2005.

E. Jackson-kuofie, Radex : A rationale-based ontology for aerospace design explanation, 2010.

P. Lago, H. Muccini, and H. Van-vliet, A scoped approach to traceability management, Journal of Systems and Software, vol.82, issue.1, pp.168-182, 2009.

L. Lamport, sometime" is sometimes "not never" : On the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '80, pp.174-185, 1980.

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.16, issue.3, pp.872-923, 1994.

J. Laprie, J. Arlat, . Blanquart, Y. Costes, Y. Crouzet et al., Guide de la sûreté de fonctionnement. Cépaduès éditions, 1995.

P. Kim-guldstrand-larsen, W. Pettersson, and . Yi, UPPAAL : status & developments, CAV, vol.1254, pp.456-459, 1997.

D. B. Lenat, V. Ramanathan, K. Guha, D. Pittman, M. Pratt et al., CYC : toward programs with common sense, Commun. ACM, vol.33, issue.8, pp.30-49, 1990.

T. Li and J. Mylopoulos, Modeling and applying security patterns using contextual goal models, Proceedings of the Seventh International i* Workshop co-located with the 26th International Conference on Advanced Information Systems Engineering, vol.1157, 2014.

D. Lightfoot, Formal specification using Z, 1991.

C. Lindig, Concept-based component retrieval, Working notes of the IJCAI-95 workshop : Formal Approaches to the Reuse of Plans, Proofs, and Programs, pp.21-25, 1995.

Z. Luo, A unifying theory of dependent types : The schematic approach, Logical Foundations of Computer Science -Tver '92, Second International Symposium, vol.620, pp.293-304, 1992.

S. Malenfant-corriveau, Proposition d'une méthode de développement d'ontologie pour un système expert en sécurité, 2017.

J. Mccarthy, Notes on formalizing context, Proceedings of the 13th International Joint Conference on Artifical Intelligence, vol.1, pp.555-560, 1993.

A. Mciver and C. Morgan, Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, 2005.

C. Meghini, F. Sebastiani, U. Straccia, and C. Thanos, A model of information retrieval based on a terminological logic, Proceedings of the 16th Annual International ACM-SIGIR Conference on Research and Development in Information Retrieval, pp.298-307, 1993.

J. Meinadier, Ingénierie et intégration des systèmes, Hermes Paris, 1998.

T. Menzies and C. Pecheur, Verification and validation and artificial intelligence, Advances in Computers, vol.65, pp.154-203, 2005.

D. Méry and M. Poppleton, Formal modelling and verification of population protocols, Johnsen and Petre, vol.158, pp.208-222

D. Méry and M. Poppleton, Towards an integrated formal method for verification of liveness properties in distributed systems : with application to population protocols. Software and System Modeling, vol.16, pp.1083-1115, 2017.

D. Méry, S. Rushikesh, and A. Tarasyuk, Integrating DomainBased Features into Event-B : a Nose Gear Velocity Case Study, Model and Data Engineering -5th International Conference, MEDI 2015, volume lncs 9344 of Model and Data Engineering -5th International Conference, MEDI 2015, pp.89-102, 2015.

P. Meseguer, Verification of multi-level rule-based expert systems, Proceedings of the Ninth National Conference on Artificial Intelligence, vol.1, pp.323-328, 1991.

R. Milner, Communication and Concurrency, 1989.

A. Mitschke, Crystal public aerospace use case development, 2016.

L. Mohand, -. , and I. Aït-sadoune, Formal modelling of domain constraints in Event-B, vol.207, pp.153-166
URL : https://hal.archives-ouvertes.fr/hal-01614550

C. Morgan, S. Thai, J. Hoang, and . Abrial, The challenge of probabilistic Event B -extended abstract, Helen Treharne

S. A. Henson and . Schneider, ZB 2005 : Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, vol.3455, pp.162-171, 2005.

K. Ghita, P. Mostéfaoui, and . Brézillon, Modeling context-based security policies with contextual graphs, Proceedings of the Second IEEE Annual Conference on Pervasive Computing and Communications Workshops, PERCOMW '04, p.28, 2004.

M. Mrissa, Médiation Sémantique Orientée Contexte pour la Composition de Services Web, 2007.

P. Geoff and . Mullery, Core-a method for controlled requirement specification, Proceedings of the 4th international conference on Software engineering, pp.126-135, 1979.

S. Myagmar, J. Adam, W. Lee, and . Yurcik, Threat modeling as a basis for security requirements, Symposium on requirements engineering for information security (SREIS), pp.1-8, 2005.

J. Mylopoulos, Information modeling in the time of the revolution, Information systems, vol.23, issue.3, pp.127-155, 1998.

A. Neumaier and . Flaviu-adrian-m?argineanm?arginean, , 2011.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, pp.371-443, 2001.

T. Nipkow and L. C. Paulson, Automated Deduction -CADE-11, 11th International Conference on Automated Deduction, vol.607, pp.673-676, 1992.

E. Note, European commission for democracy through law (venice commission)

B. Nuseibeh, J. Kramer, and A. Finkelstein, A framework for expressing the relationships between multiple views in requirements specification. Software Engineering, IEEE Transactions on, vol.20, issue.10, pp.760-773, 1994.

, Standards Coordinating Committee of the IEEE Computer Society. Ieee standard glossary of software engineering terminology, IEEE, 1990.

Y. Ouhammou, M. Ivanovic, A. Abelló, and L. Bellatreche, Model and Data Engineering -7th International Conference, vol.10563, 2017.

S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas, PVS : combining specification, proof checking, and model checking, Computer-Aided Verification, CAV '96, number 1102 in Lecture Notes in Computer Science, pp.411-414, 1996.

,. S. Sam-owre, J. M. Rajan, N. Rushby, M. K. Shankar, and . Srivas, Pvs : Combining specification, proof checking, and model checking, Proceedings of the 8th International Conference on Computer Aided Verification, CAV '96, pp.411-414, 1996.

G. Petasis, R. Möller, and V. Karkaletsis, BOEMIE : reasoning-based information extraction, NLPAR@LPNMR, volume 1044 of CEUR Workshop Proceedings, pp.60-75, 2013.

A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science, vol.13, issue.1, pp.45-60, 1981.

R. Pollack, Dependently typed records for representing mathematical structure, Theorem Proving in Higher Order Logics, 13th International Conference, vol.1869, pp.462-479, 2000.

M. Poppleton, The composition of Event-B models, Abstract State Machines, B and Z, pp.209-222, 2008.

S. Prediger, Simple concept graphs : A logic approach, Conceptual Structures : Theory, Tools and Applications, 6th International Conference on Conceptual Structures, ICCS '98, vol.1453, pp.225-239, 1998.

D. Alun and . Preece, Verification, validation, and test of knowledge-based systems, AI Magazine, vol.13, issue.4, p.77, 1992.

D. Alun, R. Preece, A. Shinghal, and . Batarekh, Principles and practice in verifying rule-based systems, Knowledge Eng. Review, vol.7, issue.2, pp.115-141, 1992.

Z. Ghassan and . Qadah, Requirements, design and implementation of an e-voting system, IADIS AC, pp.405-409, 2005.

J. Queille, The CESAR system : An aided design and certification system, Proceedings of the 2nd International Conference on Distributed Computing Systems, pp.149-161, 1981.

Q. W. Van-orman-quine, Du Point de Vue Logique, 1953.

A. Raji, Intégration des activités de preuve dans le processus de développement de logiciels pour les systèmes embarqués, 2012.

. Revva, VV&A methodological guidelines Reference Manual. . Common Validation, Verification and Accreditatation Framework for Simulation, 2004.

F. Rioult, Extraction de connaissances dans les bases de donn'ees comportant des valeurs manquantes ou un grand nombre d'attributs, 2005.
URL : https://hal.archives-ouvertes.fr/tel-00252089

R. John-alan, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

J. Roger, Exploitation de contextes et d'observateurs pour la validation formelle de modèles, 2006.

. Winston-w-royce, Managing the development of large software systems : concepts and techniques, Proceedings of the 9th international conference on Software Engineering, pp.328-338, 1987.

J. Stuart, P. Russell, and . Norvig, Artificial Intelligence -A Modern Approach (3. internat. ed.). Pearson Education, 2010.

D. Sadoun, Des spécifications en langage naturel aux spécifications formelles via une ontologie comme modèle pivot. (From natural language specifications to formal specifications via an ontology as a pivot model), 2014.

G. Salaün, M. Allemand, and C. Attiogbé, Specification of an access control system with a formalism combining CCS and CASL, IPDPS, 2002.

S. Schefer, -. Wenzl, and M. Strembeck, Modeling context-aware RBAC models for business processes in ubiquitous computing environments, Third FTRA International Conference on Mobile, Ubiquitous, and Intelligent Computing, pp.126-131, 2012.

S. Schneider and A. Sidiropoulos, Csp and anonymity, Proceedings of the 4th European Symposium on Research in Computer Security : Computer Security, ESORICS '96, pp.198-218, 1996.

S. A. Schneider, H. Treharne, H. Wehrheim, and D. M. Williams, Managing LTL properties in Event-B refinement, Integrated Formal Methods, vol.8739, pp.221-237, 2014.

. A-th, G. Schreiber, H. Schreiber, A. Akkermans, and . Anjewierden, Nigel Shadbolt, Robert de Hoog, Walter Van de Velde, and Bob Wielinga. Knowledge engineering and management : the CommonKADS methodology, 2000.

S. Shlaer and S. J. Mellor, Object Lifecycles : Modeling the World in States, 1992.

N. Singh, Reliability and Safety of Critical Device Software Systems. (Fiabilité et sûreté des systèmes informatiques critiques), 2011.
URL : https://hal.archives-ouvertes.fr/tel-01746287

G. Snelting, Concept analysis -A new framework for program understanding, Proceedings of the SIGPLAN/SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE '98, pp.1-10, 1998.

A. Souag, Vers une nouvelle génération de définition des exigences de sécurité fondée sur l'utilisation des ontologies, Actes du XXXème Congrès INFORSID, pp.583-590, 2012.

J. F. Sowa, Knowledge Representation : Logical, Philosophical and Computational Foundations, 2000.

J. F. Sowa, The Role of Logic and Ontology in Language and Reasoning, pp.231-263, 2010.

L. Stojanovic, N. Stojanovic, and D. Apostolou, Change management in e-government : Ontogov case study, vol.3, pp.74-92, 2006.

R. Studer, V. R. Benjamins, and D. Fensel, Knowledge engineering : Principles and methods. Data and knowledge engineering, vol.25, pp.161-197, 1998.

G. Alistair, S. Sutcliffe, M. Fickas, and . Sohlberg, PC-RE : a method for personal and contextual requirements engineering with some experience, Requir. Eng, vol.11, issue.3, pp.157-173, 2006.

M. Talbi, Spécification et vérification automatique des propriétés des protocoles de vote électronique en utilisant la logique ADM, 2010.

H. Ben, . Thacker, W. Scott, . Doebling, M. Francois et al., Concepts of model verification and validation, 2004.

. Amie-l-thomasson, Fiction and metaphysics, 1999.

R. Tiella, A. Villafiorita, and S. Tomasi, Specification of the control logic of an evoting system in UML : the ProVotE experience, Proceedings of the 5th International Workshop on Critical Systems Development Using Modeling Languages. Citeseer, 2006.

R. Tiella, A. Villafiorita, and S. Tomasi, Fsmc+, a tool for the generation of java code from statecharts, ACM International Conference Proceeding Series, vol.272, pp.93-102, 2007.

Y. Toussaint, Text Mining : Symbolic methods to build ontologies and to semantically annotate texts. Habilitation à diriger des recherches, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00764162

E. Tsekmezoglou and J. Iliadis, A critical view on internet voting technology, 2005.

J. Tutcher, Ontology-driven data integration for railway asset monitoring applications, BigData Conference, pp.85-95, 2014.

P. Umiliacchi, D. Lane, F. Romano, and A. Spa, Predictive maintenance of railway subsystems using an ontology based modelling approach, Proceedings of 9th world conference on railway research, pp.22-26, 2011.

, Livrable version 1.1, Avril 2007. Partie I de l'étude vote automatisé version déf, 18122006.

, Deuxième partie de l'étude vote automatisé version déf Vs, 2007.

J. Van-eijck and S. Orzan, Epistemic verification of anonymity, Electronic Notes in Theoretical Computer Science, vol.168, pp.159-174, 2007.

A. Van-lamsweerde and L. Willemet, Inferring declarative requirements specifications from operational scenarios, IEEE Transactions on Software Engineering, vol.24, issue.12, pp.1089-1114, 1998.

M. J. Van-sinderen, A. Tijmen-van-halteren, M. Wegdam, H. B. Meeuwissen, and H. Eertink, Supporting context-aware mobile applications : an infrastructure approach, IEEE Communications Magazine, vol.44, issue.9, pp.96-104, 2006.

M. Varet-pietri, L'ingénierie de la connaissance : la nouvelle épisté-mologie appliquée, Presses Univ, vol.696, 2000.

A. Villafiorita, K. Weldemariam, and R. Tiella, Development, formal verification, and evaluation of an e-voting system with VVPAT, IEEE Trans. Information Forensics and Security, vol.4, issue.4, pp.651-661, 2009.
DOI : 10.1109/tifs.2009.2034903

H. Wang, Y. Li, J. Sun, H. Zhang, and J. Pan, A semantic web approach to feature modeling and verification, Workshop on Semantic Web Enabled Software Engineering, p.46, 2005.

X. H. Wang, D. Zhang, T. Gu, and H. K. Pung, Ontology based context modeling and reasoning using OWL, 2nd IEEE Conference on Pervasive Computing and Communications Workshops, pp.18-22, 2004.

K. Weldemariam, Using Formal Methods for Building More Reliable and Secure e-Voting Systems, 2010.

R. Wille, Why can concept lattices support knowledge discovery in databases, Journal of Experimental and Theoretical Artificial Intelligence, vol.14, issue.2-3, pp.81-92, 2002.
DOI : 10.1080/09528130210164161

J. M. Wing, A specifier's introduction to formal methods, Computer, vol.23, issue.9, pp.8-23, 1990.

M. Wirsing, Algebraic specification, Handbook of Theoretical Computer Science, pp.675-788, 1990.

R. Witte, Y. Zhang, and J. Rilling, Empowering software maintainers with semantic web technologies, The Semantic Web : Research and Applications, 4th European Semantic Web Conference, vol.4519, pp.37-52, 2007.
DOI : 10.1007/978-3-540-72667-8_5

J. Zarka, Systèmes électoraux. Ellipses, coll. Mise au point, 1998.

Y. Zhao, J. Dong, and T. Peng, Ontology classification for semantic-webbased software engineering, IEEE Trans. Services Computing, vol.2, issue.4, pp.303-317, 2009.
DOI : 10.1109/tsc.2009.20