. Forme-séquentielle-réécrite-de-dcy and . .. Gcy,

, Préservation des pré et post-conditions lors du raffinement des actions, p.134

, CdC seq pour une action raffinée

L. .. Cdc-de-gcy-enfant-de,

.. .. Événement,

. .. Glossaire-de-gcy,

A. .. Du-dev-seq-sur-le-besoin-dcy,

.. .. Bilan,

.. .. Conclusion,

C. Dans-ce, nous décrivons Dev-if, un patron de développement pour le système < CdC, Liens, Spec >. Ce patron concerne les besoins décrits sous une forme conditionnelle et aide à la semiautomatisation du développement. Il est utilisé pour l'étude de cas d

, Les résultats de ce chapitre ont fait l'objet de la publication, 2017.

. Rappelons and . Su, un cahier des charges est souvent décrit en deux parties distinctes : -explicative regroupant des besoins sous forme de paragraphes, figures, tables et formules et 6.1. Description -S, 2011.

, Ceux-ci sont utilisés pour décrire les actions réalisées par le système dans le cas où la condition est vraie, -S p3 représente les paramètres décrits dans la clause then

, La première difficulté rencontrée à cette étape se résume par la question suivante : comment identifier les valeurs des paramètres dans un besoin conforme à la forme conditionnelle (6.1) proposée ? Nous donnons un premier élément de réponse à cette question en proposant de : 1. distinguer les trois clauses du besoin : son environnement, sa clause if et sa clause then, 2. localiser dans chaque clause l'élément qui change de valeur

, Ces exigences se ressemblent et concernent la pression dans un composant appelé VP transducer où VP signifie la pression veineuse. En suivant la forme (6.1), nous extrayons les différentes valeurs des paramètres de ces besoins, voir table 6.1. Notons que parmi les valeurs des paramètres de S, Prenons les deux exigences R-6 et R-10 de la figure 6.1

, Celui-ci n'apparaît pas explicitement dans l'énoncé du besoin. Il découle de notre compréhension de la suite des termes "for more than 3 seconds". Patron pour la description séquentielle d'un besoin Sommaire

. .. Initialiser-le-développement,

.. .. Prise-en-compte-d&apos;un-besoin-enfant, 3.2 Préservation des pré et post-conditions abstraites

.. .. Prise-en-compte-d&apos;un-besoin-frère,

.. .. Conclusion,

, Ce chapitre présente un de nos patrons de développement, le patron Dev-seq. Celui-ci n'est pas lié à un langage formel spécifique et s'intéresse aux besoins ayant une forme séquentielle

, Description Nous nous intéressons aux besoins décrits par une forme séquentielle pour définir notre patron de développement nommé Dev-seq. Le terme "séquentielle" signifie qu'il s'agit d'une séquence ou enchaînement d'actions dans un ordre défini. Le patron proposé permet la gestion simultanée des besoins, de leurs modèles formels associés et des liens entre eux. Celui-ci s'applique dans les phases amont du processus de développement

T. +. En, Pour notre patron, l'état de son composant Spec seq est décrit par les valeurs des paramètres des Sp i (i ? {1

, Chaque action i (Sp i ) agit sur les paramètres de Sp i . Ces derniers prennent de nouvelles valeurs

T. En and . Dans-sp-i-par-le-suffixe, Notre patron implémente son composant Spec seq en TLA + sous forme d'un Module S-new_DevSeq, voir figure 7.4. Ce module est caractérisé par : -des variables formal_pi et env_vars représentant respectivement les paramètres de Sp i et les variables d'environnement du besoin S-new, -le théorème PSinit exprime le fait que pour assurer la première action (i = 1) nous avons des contraintes sur l'environnement à respecter. Ceci permet d

, -action_n_name est raffinée par les sous-actions allant de sub-action n1 à sub-action np

, Le résultat est fourni par la figure 7.12. DCy When a door cylinder is locked in closed position and when it receives pressure from the extension hydraulic circuit, the opening doors sequence is : 1. unlock the door cylinder from the closed position 2. move it to the open position 3, En suivant la forme générique (7.1), les deux besoins DCy et GCy de la figure 7.1 sont réécrits

, GCy When a gear cylinder is locked in high position and when it receives pressure from the high hydraulic circuit, the extension gears sequence is : 1. unlock the gear cylinder from the high position 2. move it to the down position 3. lock it in the down position

, When a gear cylinder is locked in high position and when it receives pressure from the high hydraulic circuit" de GCy concernent la description d'une condition sur l'état de l'environnement englobant ces deux besoins. Il s'agit de la partie Requirement environment de la forme générique. Nous considérons que ces deux suites décrivent des pré-conditions respectives pour les deux besoins, Les suites de termes respectives

. Ls&apos;-in,

, FIGURE 7.13 -Raffinement des actions de LS'

, Préservation des pré et post-conditions abstraites

, Nous nous basons sur l'analogie effectuée avec le triplet de Hoare (voir paragraphe 7.1.2) : pour i allant de 1 à n, le résultat d'une [action_i-1_name] est une pré-condition pour l'action_i qui la suit. Par exemple, le résultat de l'[action_1_name] est une pré-condition de l'[action_2_name] et ainsi de suite. En s'inspirant de la technique de raffinement en B événementiel, Dev-seq préserve les pré et post-conditions entre les sous-actions comme suit : -le résultat de l'[action_1_name] est fourni par la sub-action 1m et -ce résultat, Nous partons de la figure 7.11 et nous nous intéressons à la préservation des pré et post-conditions abstraites entre les actions allant de 1 à n (partie gauche de cette figure) lors du raffinement

, Ceci se généralise pour toutes les autres actions

, Nous avons fixé les pré-conditions et les post-conditions des actions de LS' dans la figure 7.2. Ces pré et post-conditions ont évolué en introduisant des termes formels dans leur description. Elles sont transmises aux sous-besoins qui raffinent LS, Revenons à la forme réécrite LS' raffinée par DCy et GCy, voir figure 7.13

. Dcy, ?) the opening doors sequence is: maintained in the hydraulic extension

, FIGURE 7.14 -Préservation des pré et post-conditions lors du raffinement des actions

, Son instanciation génère les composants suivants : 7.3. Prise en compte d'un besoin enfant -Spec. Le développement de ce composant est effectué en se basant sur le raffinement de la machine associée à S-new. Ceci est offert d'une façon native en B événementiel, développement automatique des actions raffinées des besoins

. -cdc, L'introduction d'un besoin raffiné se base sur la notion de récursivité : un besoin décrit sous une forme séquentielle et entrant dans les détails d'[action_1_name] est tout d'abord réécrit en instançiant le CdC seq de la figure 7.5. Le résultat de cette instanciation est

, Cet enfant est détaillé par de nouveaux besoins allant de S-new'-1-1 à S-new'-1-m. Il devient leur parent comme présenté dans la partie (b) de la même figure, Cette récursivité permet d'introduire une hiérarchie entre les besoins. La figure 7.15 montre un cas de raffinement du besoin S-new'-1, enfant du besoin S-new', voir partie (a) de la figure

. S-new,

, The sequence name is : S-new, Besoin S-new'-1 abstrait ID Description S-new' (condition

. S-new,

, Besoin S-new'-1 raffiné nouveaux couples de termes sont automatiquement introduits dans le glossaire. Ceux-ci représentent les noms formels et leurs définitions informelles associées aux sous-actions du côté du CdC

. Prenons-le-cas-de-développement-de-gcy, Il décrit également une séquence d'actions. Ce raffinement est pris en compte par notre patron. Celui-ci génère automatique

, CdC La prise en compte du raffinement entre séquences abstraite et raffinée est montrée via une hié-rarchie entre besoins, voir figure 7.16 dans laquelle, -LS' représente LS réécrit, -GCy' définit GCy réécrit et -GCy

. Nb and L. S. Le-besoin-gcy-remplace-le-besoin,

, Vu que nous voulons garder une trace de ce besoin

, Une numérotation est introduite montrant quel besoin vient avant l'autre. Par exemple, les besoins GCy et DCy sont de même niveau mais DCy se réalise avant GCy vu que l'ouverture des portes du train d'atterrissage s'effectue avant l'extension des trains, Nous nous focalisons sur un cas où Dev-seq agit sur un modèle existant en rajoutant des détails dans le même niveau d'abstraction c

, Il s'agit d'exprimer cet ordre via l'invariant suivant nommé inv_order_i. Cet invariant est également décrit dans la figure 7.3. Celui-ci exprime que chaque pré-condition d'une action i+1 est égale à la post-condition de l'action i qui la précède, -Spec seq . En B événementiel, la notion d'ordre est exprimée dans plusieurs endroits : -Au niveau des invariants

, Revenons sur la figure 7.3. La garde grd2 de l'événement act_i_name exprime la relation d'ordre : pour effectuer cet événement il faut que la post-condition de l'événement précédent soit évaluée à vrai (TRUE)

, Liens seq . La notion d'ordre n'apparaît pas explicitement dans le glossaire

, Nous remarquons que les besoins DCy et GCy traitent tous les deux des cylindres associés aux portes et aux trains d'atterrissage. DCy est suivi temporellement par GCy. L'application du patron Dev-seq donne un nouveau système faisant évoluer le système existant sans raffinement et ajoutant de nouvelles informations apportées par DCy relativement à GCy. Le système résultant est décrit dans la figure 7.19 par : -ils sont utilisés dans les phases amont du processus de développement dès l'analyse des besoins et s, Prenons l'exemple du développement de DCy. Nous partons du système < CdC, Liens, Spec > contenant le besoin GCy développé

, Nous avons montré une définition de nos patrons en langage B événementiel. Nous avons focalisé spécifiquement sur ce langage mais nous montrons également la description et l'application du patron Dev-seq en TLA + et -ils sont définis pour automatiser le développement et réduire les risques d, -ils sont indépendants du langage de spécification utilisé

, Comme c'est le cas de plusieurs autres approches, une compréhension n'est toujours pas évidente ni directe vu que le cahier des charges souffre souvent des ambiguïtés et du manque de détails ; il faut du temps, des lectures à plusieurs reprises ainsi que l'utilisation de différents documents. Par exemple, pour le système de la machine d'hémodialyse qui décrit les cas de failles du système, nous avons eu besoin de comprendre le fonctionnement normal de cette machine avant de traiter les cas anormaux. Nous avons utilisé des images et des vidéos explicatives du processus de dialyse afin de comprendre le déroulement de ce système. La machine d'hémodialyse existait depuis plusieurs années, et son fonctionnement est connu. Ceci nous a permis d'accéder à différentes ressources de documentation. Cependant, cette méthode de documentation s'avère, Difficultés et limites Commençons par la première étape de réécriture des besoins du client

, ) les retours des activités de vérification et de validation et (4) de différentes évolutions des documents. Les outils disponibles sous la plateforme Rodin pour le langage B événe-mentiel donnent une vue d'ensemble sur les différents documents notamment les besoins et la Spec mais ne sont pas suffisants pour gérer simultanément ces documents

, Les retours de cette activité peuvent être incompréhensibles. La difficulté réside dans la localisation du constituant "coupable" causant le non-déchargement des OPs : le CdC ? la Spec ? les deux ? Aucun guide méthodologique n'est fourni pour aider à décider quel constituant revoir et corriger. D'après notre expérience, nous détectons qu'il se peut que le non-déchargement des OPs n'entre dans aucun des trois cas d'échec de preuve décrits par Abrial ; parfois ni la Spec ni le CdC sont coupables. Il s'agit des outils de preuve qui ne sont pas assez puissants pour réussir la preuve. Ceci complique à nouveau la tâche de localisation de la source d'échec de la preuve, Nous avons signalé que l'activité de vérification -à travers l'activité de preuve -concerne aussi bien la Spec que les besoins

, Nous avons utilisé des outils existants pour appliquer notre approche. Pour la suite, nous envisageons : Bibliographie, Perspectives Lors de l'application de notre contribution sur des études de cas de taille importante, nous avons obtenu des résultats encourageants, 1984.

, Systems and software engineering -Life cycle processes -Requirements engineering, 2011.

J. Abrial-;-abrial, B : passé, présent, futur, vol.22, pp.89-118, 2003.

J. Abrial, The B-book -assigning programs to meanings, 2005.

J. Abrial-;-abrial, Formal Methods in Industry : Achievements, Problems, Future, 28th International Conference on Software Engineering, pp.761-768, 2006.

J. Abrial, Train Systems, Rigorous Development of Complex FaultTolerant Systems RODIN project, pp.1-36, 2006.

J. Abrial, A System Development Process with Event-B and the Rodin Platform, Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM, pp.1-3, 2007.

J. Abrial-;-abrial and J. Abrial, Faultless Systems : Yes We Can ! IEEE Computer, vol.42, pp.30-36, 2009.

. Abrial, 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.

. Abrial, An Open Extensible Tool Environment for Event-B, Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM, pp.588-605, 2006.

. Abrial, J. Hoang-;-abrial, and T. S. Hoang, Using Design Patterns in Formal Methods : An Event-B Approach, Theoretical Aspects of Computing -ICTAC, 5th International Colloquium, pp.1-2, 2008.

. Aceituna, Model-based requirements verification method : Conclusions from two controlled experiments, Information & Software Technology, vol.56, issue.3, pp.321-334, 2014.

[. Alexander, Building Traceable Event-B Models from Requirements. Science of Computer Programming (Special Issue on Automated Verification of Critical Systems, Science of Computer Programming, vol.111, pp.100-127, 1977.

R. Banach, Hemodialysis Machine in Hybrid Event-B, Abstract State Machines, Alloy, B, TLA, VDM, and Z -5th International Conference, pp.376-393, 2016.

K. L. Beck, Embracing Change with Extreme Programming, IEEE Computer, vol.32, issue.10, pp.70-77, 1999.

;. Thayer, T. Bell, and T. Thayer, Software Requirements : Are They Really a Problem ?, ICSE-2, 2nd International Conference on Software Engineering, pp.61-68, 1976.

D. V. Ben, Formalizing new navigation requirements for NASA's space shuttle, Formal Methods Europe FME '96, vol.1051, pp.160-178, 1996.

[. Bendisposto, La validation de modèles Event-B avec le plug-in ProB pour RODIN, Technique et Science Informatiques, vol.27, issue.8, pp.1065-1084, 2008.

B. W. Boehm, An Experiment in Small-Scale Application Software Engineering, IEEE Transactions on Software Engineering, vol.7, pp.482-493, 1981.

F. Boniol and V. Wiels, Requirements Engineering and Management for Software Development Projects, ABZ Conference, vol.433, pp.1-18, 2012.

[. Cimatti, From Informal Requirements to Property-Driven Formal Validation, Formal Methods for Industrial Critical Systems, 13th International Workshop, pp.166-181, 2008.

, Towards validating a platoon of cristal vehicles using csp||b, Algebraic Methodology and Software Technology, 12th International Conference, pp.139-144, 2008.

, Reuse of early life-cycle artifacts : workproducts, methods and tools, Annals of Software Engineering, vol.5, issue.1, pp.227-251, 1998.

[. Déharbe, SMT Solvers for Rodin, Abstract State Machines, Alloy, B, VDM, and Z -Third International Conference, pp.194-207, 2012.

C. Delannoy-;-delannoy and . Delor, Software quality starts with the modelling of goal-oriented requirements, 16ème Journées Internationales "Génie Logiciel & Ingénierie de Systèmes et leurs Applications, 1976.

E. W. Dijkstra and S. Driss, From natural language specifications to formal specifications via an ontology as a pivot model, 1970.

N. Eén and N. Sörensson, An Extensible SAT-solver, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT, pp.502-518, 2003.

C. Emerson, E. A. Emerson, and E. M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Automata, Languages and Programming, p.7, 1980.

N. Colloquium and T. Netherlands, , pp.169-181

[. Fathabadi, A Systematic Approach to Atomicity Decomposition in Event-B, Software Engineering and Formal Methods -10th International Conference, pp.78-93, 2012.

M. Forsberg, K. Forsberg, and H. Mooz, The Relationship of System Engineering to the Project Cycle, Proceedings of the First Annual Symposium of National Council on System Engineering, pp.57-65, 1991.

[. Gamma, Bridging the gap between informal requirements and formal specifications using model federation, SEFM 2018 International Conference on Software Engineering and Formal Methods, 1996.

O. C. Gotel and A. Finkelstein, An analysis of the requirements traceability problem, Proceedings of the First IEEE International Conference on Requirements Engineering, ICRE '94, pp.94-101, 1994.

[. Gunter, A Reference Model for Requirements and Specifications-Extended Abstract, 4th International Conference on Requirements Engineering, vol.17, pp.37-43, 2000.

[. Hallerstede, Validation of Formal Models by Refinement Animation, Science of Computer Programming, vol.78, issue.3, pp.272-292, 2011.

M. Heisel and J. Souquières, A Method for Requirements Elicitation and Formal Specification, 18th International Conference on Conceptual Modeling, ER'99, number 1728 in LNCS Springer-Verlag, pp.309-325, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00098987

. Hoang, Event-B Patterns and their Tool Support. Software and System Modeling, vol.12, pp.229-244, 2013.

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

A. Idani-;-idani, B/UML : Mise en relation de spécifications B et de descriptions UML pour l'aide à la validation externe de développements formels en B. (B/UML : Bridging the gap between B specifications and UML graphical descriptions to ease external validation of formal B developments), 2006.

M. Jackson-;-jackson, The meaning of requirements, Annals of Software Engineering, vol.3, issue.1, pp.5-21, 1997.

M. Jastram, ProR, an Open Source Platform for Requirements Engineering based RIF, Systems Engineering Infrastructure Conference, 2010.

[. Jastram, Mixing Formal and Informal Model Elements for Tracing Requirements, vol.46, 2011.

[. Johnson, Formal methods and requirements engineering : Challenges and synergies, Journal of Systems and Software, vol.40, issue.3, pp.263-273, 1994.

J. C. Knight, Safety critical systems : challenges and directions, Proceedings of the 24th International Conference on Software Engineering, ICSE, pp.547-550, 2002.

[. Krings, From Failure to Proof : The ProB Disprover for B and Event-B, Software Engineering and Formal Methods -13th International Conference, pp.199-214, 2015.

[. Ladenberger, Validation of the ABZ landing gear system using ProB, International Journal on Software Tools for Technology Transfer (STTT), vol.19, issue.2, pp.187-203, 2017.

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

D. Leivant, Higher order logic, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume2, Deduction Methodologies, pp.229-322, 1994.

. Leuschel, M. Butler-;-leuschel, and M. Butler, ProB : A Model Checker for B, International Symposium of Formal Methods Europe, vol.2805, pp.855-874, 2003.

. Leuschel, M. Butler-;-leuschel, and M. Butler, Prob : an automated analysis toolset for the B method, STTT, vol.10, issue.2, pp.185-203, 2008.

. Lions, ARIANE 5 -Flight 501 Failure, 1996.

A. Mashkoor, The Hemodialysis Machine Case Study, Abstract State Machines, Alloy, B, TLA, VDM, and Z -5th International Conference, ABZ, pp.329-343, 2016.

J. Mashkoor, A. Mashkoor, and J. Jacquot, Validation of Formal Specifications through Transformation and Animation. Requirements Engineering, vol.16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01262115

[. Mashkoor, Refinement-based Validation of Event-B Specifications. Software and Systems Modeling, vol.33, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01262106

. Méry, . Singh, D. Méry, and N. K. Singh, Automatic code generation from eventb models, Proceedings of the 2011 Symposium on Information and Communication Technology, pp.179-188, 2011.

. Méry, . Singh, D. Méry, and N. K. Singh, Formalization of heart models based on the conduction of electrical impulses and cellular automata, Foundations of Health Informatics Engineering and Systems -First International Symposium, pp.140-159, 2011.

. Méry, . Singh, D. Méry, and N. K. Singh, Medical protocol diagnosis using formal methods, Foundations of Health Informatics Engineering and Systems -First International Symposium, pp.1-20, 2011.

. Moskewicz, Chaff : Engineering an Efficient SAT Solver, Proceedings of the 38th Design Automation Conference, pp.530-535, 2001.

P. G. Neumann, Computer Related Risks, 1995.

[. Owre, Formal Verification for Fault-Tolerant Architectures : Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering (TSE), vol.21, issue.2, pp.107-125, 1995.

D. Plagge and M. Leuschel, Validating B, Z and TLA + Using ProB and Kodkod, FM 2012 : Formal Methods -18th International Symposium, pp.372-386, 2012.

A. Pnueli, The Temporal Logic of Programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977.

[. Ponsard, Combining Models, Diagrams and Tables for Efficient Requirements Engineering : Lessons Learned from the Industry, Actes du XXXIIIème Congrès INFORSID, pp.235-250, 2015.

I. Sayar and J. Souquières, La Validation dans le Processus de Développement, Actes du XXXIVème Congrès INFORSID, pp.67-82, 2016.

I. Sayar and J. Souquières, Du cahier des charges à sa spécifi-cation, 16 ème journées AFADL, 2017.

I. Sayar and J. Souquières, La validation dans les premières étapes du processus de dévelopement. Revue ISI-DAT, numéro spécial « Décisions, argumentation et traçabilité dans l'Ingénierie des Systèmes d'Information, vol.22, pp.11-41, 2017.

K. Schwaber, SCRUM Development Process, 10th Annual ACM Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 1995.
DOI : 10.1007/978-1-4471-0947-1_11

T. Servat, BRAMA : A New Graphic Animation Tool for B Models, B 2007 : Formal Specification and Development in B, 7th International Conference of B Users, pp.274-276, 2007.
DOI : 10.1007/11955757_28

[. Singh, Formalizing the cardiac pacemaker resynchronization therapy, Digital Human Modeling -Applications in Health, Safety, Ergonomics and Risk Management : Ergonomics and Health -6th International Conference, DHM, Held as Part of HCI International, pp.374-386, 2015.
DOI : 10.1007/978-3-319-21070-4_38

C. F. Snook and M. J. Butler, UML-B : Formal Modeling and Design Aided by UML, ACM Transactions on Software Engineering and Methodology (TOSEM), vol.15, issue.1, pp.92-122, 2006.

W. Su and J. Abrial, Aircraft landing gear system : approaches with Event-B to the modeling of an industrial system, International Journal on Software Tools for Technology Transfer (STTT), vol.19, issue.2, pp.141-166, 2017.

[. Su, From Requirements to Development : Methodology and Example, 13th International Conference on Formal Engineering Methods, pp.437-455, 2011.
DOI : 10.1007/978-3-642-24559-6_30

[. Su, Formal development of a real-time operating system memory manager, 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, pp.130-139, 2015.

[. Su, Formalizing Hybrid Systems with Event-B and the Rodin Platform, Science of Computer Programming, vol.94, pp.164-202, 2014.

A. ;. Lamsweerde-;-van-lamsweerde, M. Jazayeri, A. L. Wolf, and A. Van-lamsweerde, Requirements Engineering in the Year 00 : a Research Perspective, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp.238-249, 2000.

A. Lamsweerde-;-van-lamsweerde, Requirements Engineering -From System Goals to UML Models to Software Specifications, 2009.

L. Voisin and J. Abrial, The Rodin Platform Has Turned Ten, Abstract State Machines, Alloy, B, TLA, VDM, and Z -4th International Conference, pp.1-8, 2014.
DOI : 10.1007/978-3-662-43652-3_1

L. Wang-;-wang, A Case-study of Requirements Reuse through Product Families, Annals of Software Engineering, vol.5, issue.1, pp.253-277, 1998.

N. Wirth, Program Development by Stepwise Refinement, Communications of ACM, vol.14, issue.4, pp.221-227, 1971.
DOI : 10.1007/978-1-4612-6315-9_23

URL : https://www.research-collection.ethz.ch/bitstream/20.500.11850/80846/1/eth-3026-01.pdf

S. Wright, Automatic Generation of C from Event B, Workshop on Integration of Model-based Formal Methods and Tools, pp.130-139, 2009.

F. Yang-;-yang, A Simulation Framework for the Validation of Event-B Specifications. (Un environnement de simulation pour la validation de spécifications B événementiel), 2013.
URL : https://hal.archives-ouvertes.fr/tel-01750224

. Jacquot, F. Yang, J. Jacquot, F. Yang, and J. Jacquot, An Event-B Plug-in for Creating Deadlock-Freeness Theorems, NASA Formal Methods -Third International Symposium, pp.438-452, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00623825

Y. , Proving the Fidelity of Simulations of Event-B Models, 15th International IEEE Symposium on High-Assurance Systems Engineering, pp.89-96, 2014.

P. Zave, Classification of research efforts in requirements engineering, ACM Comput. Surv, vol.29, issue.4, pp.315-321, 1997.