Publications HAL de Dominique,Méry

2016

Journal articles

ref_biblio: Yamine Aït-Ameur, Dominique Méry. Making explicit domain knowledge in formal system development. Science of Computer Programming, 2016, 121 (100--127), ⟨10.1016/j.scico.2015.12.004⟩. ⟨hal-01245832⟩
Accès au bibtex

ref_biblio: Mohamed Mosbah, Mohamed Tounsi, Dominique Mery. From Event-B specifications to programs for distributed algorithms. International journal of autonomous and adaptive communications systems, 2016, 9 (3-4), pp.223 - 242. ⟨10.1504/IJAACS.2016.079623⟩. ⟨hal-01495802⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Rosemary Monahan, Cheng Zheng. On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin. ISOLA 2016 , Bernhard Steffen and Tiziana Margaria, Oct 2016, CORFU, Greece. pp.18, ⟨10.1007/978-3-319-47166-2_57⟩. ⟨hal-01369425⟩
Accès au bibtex

ref_biblio: Didier Fass, Dominique Méry. Modelling bio-compatible and bio-integrative medical devices. European & Asian System, Software & Service Process Improvement & Innovation - EUROSPII 2016, Sep 2016, Graz, Austria. ⟨hal-03198362⟩
Accès au texte intégral et bibtex

Book sections

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Incremental Proof-Based Development for Resilient Distributed Systems. Trustworthy Cyber-Physical Systems Engineering, Taylor and Francis Group, 2016, Trustworthy Cyber-Physical Systems Engineering. ⟨hal-01246669⟩
Accès au bibtex

2015

Conference papers

ref_biblio: Dominique Méry, Sawant Rushikesh, Anton Tarasyuk. Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study. Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. pp.89-102. ⟨hal-01245991⟩
Accès au bibtex

ref_biblio: Dominique Mery, Neeraj Kumar Singh. Analyzing Requirements Using Environment Modelling. DHM 2015 - 6th International Conference on Digital Human Modeling Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, Aug 2015, Los Angeles, United States. pp.345-357, ⟨10.1007/978-3-319-21070-4_35⟩. ⟨hal-02354252⟩
Accès au texte intégral et bibtex

ref_biblio: Didier Fass, Dominique Méry. Integrated human systems design : bridging the gap between formal and experimental approaches. NASA AMES Research Center, Human Systems Integration Division,, 2015, MOFETT FIELD - Etats-Unis d'Amérique, Unknown Region. ⟨hal-01507847⟩
Accès au bibtex

Books

ref_biblio: Catherine Dubois, Paolo Masci, Dominique Méry (Dir.). Second International Workshop on Formal Integrated Development Environment. EPTCS, 187, 2015, EPTCS ⟨10.4204/EPTCS.187⟩. ⟨hal-01246691⟩
Accès au bibtex

2014

Journal articles

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version). Computer Science and Information Systems, 2014, Computer Science and Information System, 11 (1), pp.251-270. ⟨10.2298/CSIS130122007A⟩. ⟨hal-00924525⟩
Accès au bibtex

ref_biblio: Dominique Méry, Bernhard Schätz, Alan Wassyng. The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062). Dagstuhl Reports, 2014, 4 (2), pp.17--37. ⟨hal-01097629⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Formal Evaluation of Landing Gear System. SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam. ⟨hal-01097645⟩
Accès au bibtex

ref_biblio: Yamine Aït-Ameur, John Paul Gibson, Dominique Méry. On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems. 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Specialized Techniques and Applications (ISoLA 2014), Oct 2014, Corfu, Greece. pp.604-618, ⟨10.1007/978-3-662-45231-8_50⟩. ⟨hal-01097624⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry. Playing with State-Based Models for Designing Better Algorithms. Model and Data Engineering - 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. pp.1-3. ⟨hal-01097625⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. The Semantics of Refinement Chart. HCI International, Jun 2014, Heraklion, Greece. pp.415-426, ⟨10.1007/978-3-319-07725-3_42⟩. ⟨hal-00995176⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Modeling an Aircraft Landing System in Event-B. ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. pp.154-159. ⟨hal-00985010⟩
Accès au bibtex

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Analysis of Self-* and P2P Systems using Refinement. ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Yamine AIT AMEUR and Klaus-Dieter SCHEWE, Jun 2014, Toulouse, France. pp.117-123, ⟨10.1007/978-3-662-43652-3_9⟩. ⟨hal-01018125⟩
Accès au bibtex

Book sections

ref_biblio: Neeraj Kumar Singh, Dominique Méry. Event B (english version). Jean-Louis Boulanger. Formal Methods Applied to Complex Systems, Wiley, 2014, Formal Methods Applied to Complex Systems, 9781119002727. ⟨10.1002/9781119002727.ch10⟩. ⟨hal-01216779⟩
Accès au bibtex

Books

ref_biblio: Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry (Dir.). Proceedings 1st Workshop on Formal Integrated Development Environment. Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. EPTCS, 149, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩. ⟨hal-00987531⟩
Accès au bibtex

Proceedings

ref_biblio: Gabriel Ciobanu, Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014. Gabriel Ciobanu; Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, Sep 2014, Bucharest, Romania. 8687, Springer, 2014, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-10882-7⟩. ⟨hal-01097627⟩
Accès au bibtex

Reports

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Modelling an Aircraft Landing System in Event-B (Full Report). [Research Report] 2014. ⟨hal-00971787⟩
Accès au texte intégral et bibtex

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Analysis of Self-* and P2P Systems using Reﬁnement (Full Report). [Research Report] 2014. ⟨hal-01018162⟩
Accès au texte intégral et bibtex

2013

Journal articles

ref_biblio: Gérard Morel, Jean-Marc Dupont, Romain Lieber, Fabien Bouffaron, Dominique Méry, et al.. Spécification d'exigences physico-physiologiques d'interaction homme-machine en ingénierie système. Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2013, Mars 2013 (104), pp.29-39. ⟨hal-00805851⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Formal Speciﬁcation of Medical Systems by Proof-Based Reﬁnement. ACM Transactions on Embedded Computing Systems (TECS), 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩. ⟨inria-00637756⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Ideal Mode Selection of a Cardiac Pacing System. 4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. pp.258-267, ⟨10.1007/978-3-642-39173-6_31⟩. ⟨hal-00862077⟩
Accès au bibtex

ref_biblio: Dominique Méry, Monahan Rosemary. Transforming EVENT B Models into Verified C# Implementations. VPT 2013 - First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73. ⟨hal-00862050⟩
Accès au bibtex

ref_biblio: Mohammed Tounsi, Mohammed Mosbah, Dominique Méry. From Event-B Specifications to Programs for Distributed Algorithms. WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩. ⟨hal-00862056⟩
Accès au bibtex

ref_biblio: Dominique Méry, Mike Poppleton. Formal Modelling and Verification of Population Protocols. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. ⟨hal-00813033⟩
Accès au bibtex

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. ⟨hal-00819256⟩
Accès au bibtex

Book sections

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Event B. Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7. ⟨hal-00926335⟩
Accès au bibtex

2012

Conference papers

ref_biblio: Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, Camel Tanougast. Formal Verification of Fault Tolerant NoC-based Architecture. First International Workshop on Mathematics and Computer Science (IWMCS2012), Mostefa BELARBI - University of Tiaret - Algeria, Dec 2012, Tiaret, Algeria. ⟨hal-00763092⟩
Accès au texte intégral et bibtex

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques. PDCAT 2012 : The Thirteenth International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2012, Beijing, China. ⟨hal-00734131⟩
Accès au texte intégral et bibtex

ref_biblio: Yamine Aït-Ameur, Dominique Méry. Handling Heterogeneity in Formal Developments of Hardware and Software Systems. ISoLA - 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - 2012, Tiziana Margaria and Bernhard Steffen, Oct 2012, Amirandes, Heraklion, Greece. pp.327-328, ⟨10.1007/978-3-642-34032-1_33⟩. ⟨hal-00743810⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Critical systems development methodology using formal techniques. 3rd International Symposium on Information and Communication Technology - SoICT 2012, Aug 2012, Ha Long, Vietnam. pp.3-12, ⟨10.1145/2350716.2350720⟩. ⟨hal-00747305⟩
Accès au bibtex

Book sections

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Formalization of Heart Models Based on the Conduction of Electrical Impulses and Cellular Automata. Liu; Zhiming and Wassyng; Alan. Foundations of Health Informatics Engineering and Systems}, 7151, Springer Berlin Heidelberg, pp.140-159, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. ⟨10.1007/978-3-642-32355-3_9⟩. ⟨hal-00762821⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Medical Protocol Diagnosis Using Formal Methods. Liu; Zhiming and Wassyng; Alan. Foundations of Health Informatics Engineering and Systems, 7151, Springer Berlin Heidelberg, pp.1-20, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. ⟨10.1007/978-3-642-32355-3_1⟩. ⟨hal-00762822⟩
Accès au bibtex

Books

ref_biblio: Dimitra Giannakopoulou, Dominique Méry. FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Dimitra Giannakopoulou and Dominique Méry. Springer, 7436, pp.488, 2012, LNCS - Lecture Notes in Computer Science, 978-3-642-32758-2. ⟨10.1007/978-3-642-32759-9⟩. ⟨hal-00743808⟩
Accès au bibtex

Reports

ref_biblio: Jean-Marc Dupont, Romain Lieber, Gérard Morel, Dominique Méry, Fabien Bouffaron. Spécification d'un Processus Technico-Physiologique de Perception de Fermeture et Verrouillage d'un capot moteur en situation de maintenance aéronautique. 2012. ⟨hal-00769223⟩
Accès au bibtex

2011

Journal articles

ref_biblio: Mohamed Tounsi, Mohamed Mosbah, Dominique Méry. Proving Distributed Algorithms by Combining Reﬁnement and Local Computations. Electronic Communications of the EASST, 2011, 35, pp.ISSN 1863-2122. ⟨hal-00644187⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. A generic framework: from modeling to code. Innovations in Systems and Software Engineering (ISSE), 2011, pp.1-9. ⟨inria-00637761⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Formal Development and Automatic Code Generation : Cardiac Pacemaker. International Conference on Computers and Advanced Technology in Education (ICCATE, 2011), Nov 2011, Beijing, China. ⟨inria-00638486⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Automatic Code Generation from Event-B Models. SoICT 2011, Hanoi University, Oct 2011, Hanoi, Vietnam. ⟨inria-00637765⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Analysis of DSR Protocol in Event-B. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. pp.401-415. ⟨inria-00637768⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. EB2J : Code Generation from Event-B to Java. SBMF - Brazilian Symposium on Formal Methods, CBSoft - Brazilian Conference on Software: Theory and Practice, Sep 2011, São Paulo, Brazil. ⟨inria-00638467⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Medical Protocol Diagnosis using Formal Methods. International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa. ⟨inria-00638478⟩
Accès au bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Formalisation of the Heart based on Conduction of Electrical Impulses and Cellular-Automata. International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa. ⟨inria-00638473⟩
Accès au bibtex

ref_biblio: Dominique Méry, Mohamed Mosbah, Mohamed Tounsi. Refinement-based Verification of Local Synchronization Algorithms. 17TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS, Jun 2011, Limerick, Ireland. à paraître. ⟨hal-00579252⟩
Accès au bibtex

Book sections

ref_biblio: Dominique Méry, Didier Fass. Top modèle et Top simulation : la momie de Lunéville Observation, Modélisation, Simulation et Validation. Francis JANOT. La Dame d'Antinoé : une "momie" au Château de Lunéville, Presse universitaire de Nancy, pp.132, 2011, Archéologie, Espaces, Patrimoines, 978-2-8143-0088-0. ⟨hal-00744242⟩
Accès au texte intégral et bibtex

Reports

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Technical Report on Formalisation of the Heart using Analysis of Conduction Time and Velocity of the Electrocardiography and Cellular-Automata. [Technical Report] 2011. ⟨inria-00600339⟩
Accès au texte intégral et bibtex

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry. Stepwise Development Of Distributed Vertex Coloring Algorithms (Full Report). [Technical Report] LORIA - Université de Lorraine. 2011, pp.90. ⟨inria-00606254v2⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Technical Report on Interpretation of the Electrocardiogram (ECG) Signal using Formal Methods. [Technical Report] 2011. ⟨inria-00584177⟩
Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio: Manamiary Bruno Andriamiarina, Dominique Méry. Stepwise Development of Distributed Vertex Colouring Algorithms (Abstract). 2011. ⟨inria-00606201⟩
Accès au texte intégral et bibtex

2010

Journal articles

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Functional Behavior of a Cardiac Pacing System. International Journal of Discrete Event Control Systems (IJDECS), 2010. ⟨inria-00540007⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Real-Time Animation for Formal Specification. Complex Systems Design & Management 2010, Oct 2010, Paris, France. pp.49-60, ⟨10.1007/978-3-642-15654-0_3⟩. ⟨inria-00540005⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Trustable Formal Specification for Software Certification. 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, Oct 2010, Heraklion, Crete, Greece. pp.312-326, ⟨10.1007/978-3-642-16561-0_31⟩. ⟨inria-00540008⟩
Accès au bibtex

ref_biblio: Dominique Méry, Mohammed Mosbah, Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Sep 2010, Dusseldorf, Germany. ⟨inria-00547302⟩
Accès au bibtex

ref_biblio: Nazim Benaissa, Dominique Méry. Proof-Based Design of Security Protocols. 5th International Computer Science Symposium in Russia, CSR 2010, Farid Ablayev, Jun 2010, KAZAN, Russia. pp.25-36. ⟨inria-00542919⟩
Accès au bibtex

Other publications

ref_biblio: Dominique Méry, Neeraj Kumar Singh. EB2C : A Tool for Event-B to C Conversion Support. 2010. ⟨inria-00540006⟩
Accès au texte intégral et bibtex

Books

ref_biblio: Dominique Méry, Stephan Merz (Dir.). Integrated Formal Methods. Dominique Méry and Stephan Merz. Springer, 6396, pp.335, 2010, Lecture Notes in Computer Science, 978-3-642-16264-0. ⟨10.1007/978-3-642-16265-7⟩. ⟨inria-00539785⟩
Accès au bibtex

Reports

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. [Research Report] 2010. ⟨inria-00465061v2⟩
Accès au texte intégral et bibtex

2009

Journal articles

ref_biblio: Dominique Méry. Reﬁnement-Based Guidelines for Algorithmic Systems. International Journal of Software and Informatics (IJSI), 2009, 3 (2-3), pp.197-239. ⟨inria-00426383⟩
Accès au bibtex

ref_biblio: Dominique Méry. A Simple Refinement-based Method for Constructing Algorithms. Sigcse Bulletin, 2009, inroads — SIGCSE Bulletin, 41 (2), pp.51-59. ⟨10.1145/1595453.1595462⟩. ⟨inria-00426384⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Cyril Proch. System-on-chip design by proof-based reﬁnement. International Journal on Software Tools for Technology Transfer, 2009, 11 (3), pp.217-238. ⟨10.1007/s10009-009-0104-7⟩. ⟨inria-00426385⟩
Accès au bibtex

Conference papers

ref_biblio: Nazim Benaissa, Dominique Méry. Cryptologic protocols analysis using proof-based patterns. Seventh International Andrei Ershov Memorial Conference "PERSPECTIVES OF SYSTEM INFORMATICS" - PSI 2009, Jun 2009, Novosibirsk, Russia. ⟨inria-00431253⟩
Accès au bibtex

ref_biblio: Nazim Benaissa, Dominique Méry. Cryptographic Protocols Analysis in Event B. Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Jun 2009, Novosibisrk, Russia. ⟨inria-00431264⟩
Accès au bibtex

ref_biblio: Mohamed Tounsi, Ahmed Hadj Kacem, Mohamed Mosbah, Dominique Méry. A Refinement Approach for Proving Distributed Algorithms : Examples of Spanning Tree Problems. Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Feb 2009, Düsseldorf, Germany. ⟨hal-00361933⟩
Accès au bibtex

ref_biblio: Nazim Benaissa, Dominique Méry. Développement combiné et prouvé de systèmes transactionnels cryptologiques. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2009, Jan 2009, Toulouse, France. ⟨inria-00426405⟩
Accès au texte intégral et bibtex

Reports

ref_biblio: Julien Siebert, Joris Rehm, Vincent Chevrier, Laurent Ciarletta, Dominique Méry. AA4MM coordination model and event-B specification. [Research Report] RR-7081, INRIA. 2009, pp.22. ⟨inria-00435569v3⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry, Neeraj Kumar Singh. Pacemaker's Functional Behaviors in Event-B. [Research Report] 2009. ⟨inria-00419973v2⟩
Accès au texte intégral et bibtex

2008

Journal articles

ref_biblio: Dominique Cansell, Paul Gibson, Dominique Méry. Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface. Electronic Notes in Theoretical Computer Science, 2008, 183, pp.39-55. ⟨10.1016/j.entcs.2007.01.060⟩. ⟨inria-00594892⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry. Teaching programming methodology using Event B. The B Method: from Research to Teaching, Henri Habrias, Jul 2008, Nantes, France. ⟨inria-00287231v2⟩
Accès au texte intégral et bibtex

Book sections

ref_biblio: Dominique Cansell, Dominique Méry. The Event-B Modelling Method - Concepts and Case Studies. Dines Bjoerner and Martin Henson. Logics of Specification Languages, Springer, pp.33-140, 2008, Monographs in Theoretical Computer Science. ⟨inria-00579550⟩
Accès au bibtex

Reports

ref_biblio: Dominique Cansell, Dominique Méry, Joris Rehm. Intégration de contraintes temps-réel au sein d'un processus de développement incrémental basé sur la preuve (Livrable 2). [Rapport de recherche] 2008. ⟨inria-00593372⟩
Accès au texte intégral et bibtex

ref_biblio: Nazim Benaissa, Dominique Méry. Développement incrémental prouvé de systèmes répartis : le cas Mondex. [Rapport de recherche] 2008, pp.13. ⟨inria-00336655⟩
Accès au texte intégral et bibtex

2007

Journal articles

ref_biblio: Thierry Lecomte, Dominique Méry, Dominique Cansell. Patrons de conception prouvés. Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2007, Ingénierie dirigée par les modèles, 81 (juin 2007), pp.14-18. ⟨inria-00184827⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Incremental Parametric Development of Greedy Algorithms. Electronic Notes in Theoretical Computer Science, 2007, roceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), 185, pp.47-62. ⟨10.1016/j.entcs.2007.05.028⟩. ⟨inria-00594883⟩
Accès au bibtex

ref_biblio: Dominique Méry, Stephan Merz. Specification and Refinement of Access Control. Journal of Universal Computer Science, 2007, 13 (8), pp.1073-1093. ⟨inria-00147824⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Cansell, Paul Gibson, Dominique Méry. Formal verification of tamper-evident storage for e-voting. 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. pp.329-338, ⟨10.1109/SEFM.2007.21⟩. ⟨inria-00184833⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Proved-Patterns-Based Development for Structured Programs.. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Ural State University (USU) ; Institute of Mathematics and Mechanics of Ural Branch of Russian Academy of Sciences, Sep 2007, Ekaterinburg, Russia. pp.104-114, ⟨10.1007/978-3-540-74510-5_13⟩. ⟨inria-00168307⟩
Accès au bibtex

ref_biblio: Nazim Benaissa, Dominique Cansell, Dominique Mery. Integration of Security Policy into System Modeling. The 7th International B Conference - B2007, Jan 2007, Besançon, France. ⟨inria-00155143⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Joris Rehm. Time Constraint Patterns for Event B Development. 7th International Conference of B Users, January 17-19, 2007, 2007, Besançon, France. pp.140-154, ⟨10.1007/11955757_13⟩. ⟨hal-00149163⟩
Accès au texte intégral et bibtex

Book sections

ref_biblio: Dominique Cansell, Dominique Méry. Designing old and new distributed algorithms by replaying an incremental proof-based development. Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS. ⟨inria-00174023⟩
Accès au bibtex

2006

Journal articles

ref_biblio: Dominique Cansell, Dominique Méry. Formal and Incremental Construction of Distributed Algorithms: On the Distributed Reference Counting Algorithm. Theoretical Computer Science, 2006, ⟨10.1016/j.tcs.2006.08.015⟩. ⟨inria-00093164⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Cansell, Dominique Méry. Incremental Parametric Development of Greedy Algorithms. 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62. ⟨inria-00089497⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Evrot, Jean-François Pétin, Dominique Méry. Formal specification of safe manufacturing machines using the B method : application to a mechanical press. May 2006, pp.CDROM. ⟨hal-00120743⟩
Accès au bibtex

ref_biblio: Dominique Méry, Stephan Merz. Event Systems and Access Control. Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, Mar 2006, Vienna/Austria, pp.40-54. ⟨inria-00001262⟩
Accès au texte intégral et bibtex

Book sections

ref_biblio: Dominique Cansell, Dominique Méry. Event B. Henri Habrias and Marc Frappier. Software Specification Methods, HERMES, 2006, 1-905209-34-7. ⟨inria-00096696⟩
Accès au bibtex

Lectures

ref_biblio: Dominique Cansell, Dominique Méry. Tutorial on the event-based B method. IFIP FORTE 2006 Paris, 2006. ⟨inria-00092846⟩
Accès au texte intégral et bibtex

2005

Journal articles

ref_biblio: Dominique Méry, Dominique Cansell, Cyril Proch, Denis Abraham, Patrick Ditsch. The challenge of QoS for digital television services. EBU Technical Review, 2005, 302 (Avril), 11 p. ⟨inria-00001252⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Cyril Proch. Un système d'analyse de la qualité: de la norme au produit en passant par le raffinement. Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2005, 73, pp.44-50. ⟨inria-00000196⟩
Accès au texte intégral et bibtex

Conference papers

ref_biblio: Dominique Cansell, Dominique Méry, Cyril Proch. Modelling SystemC scheduler by refinement. IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05, Sep 2005, Columbia/USA. ⟨inria-00000564⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Formal and Incremental Construction of a Distributed Reference Counting Algorithm.. APPSEM 2005, Martin Hofmann, Sep 2005, Frauenchiemsee Germany. ⟨inria-00000788⟩
Accès au bibtex

ref_biblio: Denis Abraham, Dominique Cansell, Patrick Ditsch, Dominique Méry, Cyril Proch. Synthesis of the QoS for digital TV services. First International Workshop on Incentive Based Computing - IBC'05, Sep 2005, Amsterdam/Hollande. ⟨inria-00000565⟩
Accès au bibtex

ref_biblio: Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Refinement and Reachability in Event_B. ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users, Apr 2005, Guilford/UK, pp.222-241, ⟨10.1007/11415787_14⟩. ⟨inria-00001245⟩
Accès au bibtex

ref_biblio: Loïc Fejoz, Dominique Méry, Stephan Merz. DIXIT: a Graphical Toolkit for Predicate Abstractions. Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48. ⟨inria-00000767⟩
Accès au texte intégral et bibtex

Reports

ref_biblio: Dominique Cansell, Dominique Méry. The invoice case study modelling in Event B. [Research Report] 2005. ⟨inria-00000857⟩
Accès au texte intégral et bibtex

2004

Conference papers

ref_biblio: Dominique Cansell, Jean-François Culat, Dominique Méry, Cyril Proch. Derivation of SystemC code from abstract system models. Forum on specification and Design Languages - FDL'04, 2004, Lille, France, 12 p. ⟨inria-00107780⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Méry. Synthèse formelle par raffinement de modèles et de logiciels pour l'automaisation. Journées d'Etude "Automatique et Informatique", Club des Enseignants et des Chercheurs en Electronique, Electrotechnique et Automatique, Section Automatique, 2004, Cachan, France. ⟨inria-00100064⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Tutorial on the event-based B method : Concepts and Case Studies. Logics of Formal Software Specification Languages - LFSL'2004, 2004, The High Tatras, Slovakia. ⟨inria-00100065⟩
Accès au bibtex

ref_biblio: Gérard Morel, Dominique Méry, Jean-Baptiste Léger, Thierry Lecomte. Proof-Oriented Fault-Tolerant Systems Engineering : Rationales, Experiments and Open Issues. 7th IFAC Symposium on Cost Oriented Automation - COA'2004, 2004, Gatineau, Québec, Canada. ⟨inria-00100068⟩
Accès au bibtex

Reports

ref_biblio: Cyril Proch, Dominique Cansell, Dominique Mery. Projet RNRT EQUAST ; SP2 Spécification incrémentale du système. [Interne] A04-R-237 || proch04a, 2004. ⟨inria-00100222⟩
Accès au bibtex

2003

Journal articles

ref_biblio: Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. Formal Aspects of Computing, 2003, 14 (3), pp.215-227. ⟨inria-00099531⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Foundations of the B method. Computing and Informatics, 2003, 22, 31 p. ⟨inria-00099794⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Cansell, Camel Tanougast, Dominique Méry, Cyril Proch, Hassan Rabah, et al.. Proof-based design of a microelectronic architecture for mpeg-2 bit-rate measurement. Forum on specification and Design Languages-FDL'03, Sep 2003, Frankfurt, Germany. ⟨hal-03983966⟩
Accès au bibtex

ref_biblio: Dominique Méry, Nidhal Rezg, Xiaolan Xie. Modélisation des systèmes réactifs. 4ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2003, 2003, Metz, France, 568 p. ⟨inria-00099541⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Designing event-driven systems by combining coordination and refinement. 2nd International Workshop on Refinement of Critical Systems: Methods, Tools and Developments - RCS'03, 2003, Turku, Finland. ⟨inria-00099835⟩
Accès au bibtex

ref_biblio: Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Formal derivation of spanning trees algorithms. Third International Conference of B and Z Users - ZB'2003, Marina Walden, 2003, Turku, Finland, pp.457-476. ⟨inria-00099793⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Camel Tanougast, Yves Berviller, Dominique Méry, Cyril Proch, et al.. Proof-based design of a microelectronic architecture for MPEG-2 bit-rate measurement. Forum on specification and Design Languages - FDL'03, 2003, Frankfurt, Germany, France. 12 p. ⟨inria-00099834⟩
Accès au bibtex

2002

Conference papers

ref_biblio: Hervé Panetto, Jean-François Pétin, Dominique Méry. Formalisation of enterprise modelling standards using UML and the B method.. 8th International Conference on Concurrent Enterprising, ICE2002, Jun 2002, Rome, Italy. pp.93-101. ⟨hal-00120944⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Méry, Airy Weinzoepflen. Incremental Proof of the Producer/Consumer Property for the PCI Protocol. 2nd International Conference of B and Z Users - ZB 2002, 2002, Grenoble, France, pp.22-41. ⟨inria-00100888⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Integration of the proof process in the system development through refinement steps. 5th Forum on Specification and Design Language - Workshop SFP in FDL'02, 2002, Marseille, France, 12 p. ⟨inria-00100945⟩
Accès au bibtex

Reports

ref_biblio: Dominique Cansell, Dominique Méry. Développement de fonctions définies récursivement en B : Application du B événementiel. [Interne] A02-R-347 || cansell02b, 2002, 25 p. ⟨inria-00101076⟩
Accès au bibtex

2001

Conference papers

ref_biblio: Dominique Cansell, Jacques Jaray, Dominique Mery. Utilisation de B pour l'aide à la spécification d'un système de diagnostic. Approche Formelles dans l'Assistance au Développement de Logiciels - AFADl'2001, Jun 2001, Nancy, France, 15 p. ⟨inria-00100931⟩
Accès au bibtex

ref_biblio: Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Specification and Design of the Leader Election Protocol of IEEE 1394. IEEE 1394 (FireWire) Workshop: International Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001, Berlin, Germany, 3 p. ⟨inria-00100598⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Airy Weinzoepflen. Modélisation et analyse de la documentation technique d'un système. Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2001, 2001, Toulouse, France, 16 p. ⟨inria-00101089⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Stephan Merz. Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams. Integrating Diagrammatic and Formal Specification Techniques, GI Fachgruppe 0.1.7 Specification and Semantics, 2001, Wien, Austria, pp.39-45. ⟨inria-00110548⟩
Accès au bibtex

2000

Journal articles

ref_biblio: Dominique Cansell, Dominique Méry, Stephan Merz. Diagrams Refinement for the Design of Reactive Systems. Journal of Universal Computer Science, 2000, 7 (2), pp.159-174. ⟨inria-00099265⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Cansell, Dominique Méry, Stephan Merz. Predicate diagrams for the verification of reactive systems. Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, pp.380-397. ⟨inria-00099125⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Stephan Merz. Predicate diagrams. Workshop on Requirement, Design, Correct Construction & Verification, M.V. Cengarle, 2000, Munich, Germany. ⟨inria-00099263⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Playing with abstraction and refinement for managing features interactions. A methodological approach to feature interaction problem. International Conference on B & Z Users - ZB'2000, 2000, York, GB, pp.148-167. ⟨inria-00099157⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Christophe Tabacznyj. Abstraction and Refinement of Concurrent Programs and Formal Specification. Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, Dominique Méry & Beverly Sanders, 2000, Cancun, Mexico, pp.1037-1038. ⟨inria-00099262⟩
Accès au bibtex

ref_biblio: Paul Gibson, Geoff Hamilton, Dominique Méry. A taxonomy for triggered interactions using fair object semantics. Feature Interactions in Telecommunications & Software Systems VI, 2000, Glasgow, UK, 20 p. ⟨inria-00099267⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry, Stephan Merz. Verifying Reactive Systems Using Predicate Diagrams. FM-TOOLS'2000, Wolfgang Reif & Gerhard Schellhorn, 2000, Ulm, 5 p. ⟨inria-00099261⟩
Accès au bibtex

Book sections

ref_biblio: Dominique Cansell, Dominique Méry. Abstraction and refinement of features. Stephen, Gilmore et Mark, Ryan. Language Constructs for Designing Features, Springer, 2000. ⟨inria-00099264⟩
Accès au bibtex

ref_biblio: John Paul Gibson, Dominique Méry. Fair Objects. H. Zedan & A. Cau. Object-oriented technology and computing systems re-engineering, Horwood Publishing Ltd, 2000, Computer Science & Electronic Engineering. ⟨inria-00099324⟩
Accès au bibtex

Reports

ref_biblio: Dominique Cansell, Jacques Jaray, Dominique Méry. Rapport final de contrat Cifre entre le LORIA et Peugeot SA et de contrat d'expertise sur l'utilisation de la méthode B.. [Contrat] A00-R-047 || cansell00a, 2000, 34 p. ⟨inria-00099343⟩
Accès au bibtex

1999

Conference papers

ref_biblio: Dominique Méry, Yassine Mokhtari. Validation of formal specifications. AAAI'99, Fall Symposium, Nov 1999, none, 5 p. ⟨inria-00108115⟩
Accès au texte intégral et bibtex

ref_biblio: Raphaël Couturier, Bertrand Couturier, Dominique Méry. A compiler for parallel Unity programs using OpenMp. Parallel and Distributed Processing Techniques & Applications - PDPTA'99, Jul 1999, Las Vegas, USA, 21 p. ⟨inria-00098760⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Paul Gibson, Dominique Méry, Yassine Mokhtari. Animating formal specifications : a telephone simulation case study. 13th European Simulation Multiconference - ESM'99, Jun 1999, Warsaw, Poland, pp.139--145. ⟨inria-00108114⟩
Accès au texte intégral et bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Abstract animator for temporal specifications Application to TLA. International Symposium on Static Analysis - SAS'99, Gilberto Fil{é} & Agostino Cortesi, 1999, Venise, Italie, pp.284-299. ⟨inria-00098953⟩
Accès au bibtex

ref_biblio: Jean-Paul Gibson, Dominique Méry. Formal modelling of services for getting a better understanding of the feature interaction problem - multi-view approach. Andrei Ershov Third International Conference, Perspectives of system Informatics - PSI'99, 1999, Novosibirsk, Russia, pp.155-179. ⟨inria-00098998⟩
Accès au bibtex

ref_biblio: John Paul Gibson, Geoff Hamilton, Dominique Méry. Integration Problems in Telephone Feature requirements. Workshop on Integrated Formal Methods - IFM'99, 1999, York, England, 19 p. ⟨inria-00098882⟩
Accès au bibtex

ref_biblio: Dominique Méry. Requirements for a Temporal B
Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems : Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems. Integrated Formal Methods - IFM'99, A. Galloway, 1999, York, UK, 20 p. ⟨inria-00108066⟩
Accès au bibtex

ref_biblio: Patrick Lamboley, Jean-François Pétin, Dominique Méry. Towards a formal engineering framework for process automation. Seventh IEEE International Conference on Emerging Technologies & Factory Automation - ETFA'99, 1999, Barcelona, Spain, 8 p. ⟨inria-00098874⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Abstract Animator for Temporal Specifications. Workshop on Modelling & Verification, Françoise Bellegarde, Olga Kouchnarenko & Jacques Julliand, 1999, Besançon, France. ⟨inria-00098918⟩
Accès au bibtex

Books

ref_biblio: Dominique Méry (Dir.). Special Issue FMPPTA'98. World Scientific, 1999, Parallel Processing Letters. ⟨inria-00108068⟩
Accès au bibtex

ref_biblio: Dominique Méry, Guy-René Perrin (Dir.). Edition Spéciale RenPar'10. Hermès, 1999, TSI. ⟨inria-00108067⟩
Accès au bibtex

1998

Journal articles

ref_biblio: Bruno Mermet, Dominique Méry, Dmitri Samborski. Spécification de services : une approche avec B. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 1998, 17 (9), pp.1157-1180. ⟨inria-00098448⟩
Accès au bibtex

Conference papers

ref_biblio: Dominique Méry, Jean-François Pétin. Formal engineering methods for modelling and verification of control systems. 9th symposium on information control problems in manufacturing Advances in Industrial Engineering - INCOM'98, 1998, Nancy/France, 6 p. ⟨inria-00098619⟩
Accès au bibtex

ref_biblio: Dominique Cansell, Dominique Méry. Interprétation de spécifications temporelles à l'aide d'un outil de preuve. AFADl'98, 1998, none, 13 p. ⟨inria-00098541⟩
Accès au bibtex

ref_biblio: Dominique Méry, Jean-Paul Gibson. Fair Objects. Object Technology 98 (Colloquim on Object Technology System Re-engineering), 1998, none, 16 p. ⟨inria-00098620⟩
Accès au bibtex

ref_biblio: Raphaël Couturier, Dominique Méry. An experiment in parallelizing an application using formal methods. International Conference on Computer Aided Verification - CAV'98, 1998, Vancouver, Canada, 10 p. ⟨inria-00098540⟩
Accès au bibtex

ref_biblio: Jean-François Pétin, Gérard Morel, Dominique Méry, Patrick Lamboley. Process control engineering: contribution to a formal structuring framework with the B method. The 2nd International B Conference, 1998, Montpellier, France. pp.198-209. ⟨inria-00098406⟩
Accès au bibtex

ref_biblio: Jean-Paul Gibson, Dominique Méry. Always and Eventually in Object Requirements. Rigorous Object Oriented Methods, 1998, none, 20 p. ⟨inria-00098617⟩
Accès au bibtex

ref_biblio: Bruno Mermet, Dominique Méry. Service specifications to B, or not to B. Second Workshop on Formal Methods in Software Practice, 1998, Clearwater Beach, Florida, USA, 8 p. ⟨inria-00098409⟩
Accès au bibtex

ref_biblio: Raphaël Couturier, Dominique Méry. Parallelization of a Monte Carlo simulation of a spins system. Parallel and Distributed Processing Techniques and Applications - PDPTA'98, 1998, Las Vegas, USA, 5 p. ⟨inria-00098542⟩
Accès au bibtex

ref_biblio: Jean-Paul Gibson, Dominique Méry. Teaching Formal Methods: Lessons to learn. Irish Workshop For Formal Methods 1998, 1998, Cork, Irlande, 16 p. ⟨inria-00098616⟩
Accès au bibtex

Books

ref_biblio: Dominique Méry, Beverly Sanders (Dir.). Third International Workshop on Formal Methods for Parallel Programming : Theory and Applications. Springer Verlag, 100 p, 1998, Lecture Notes in Computer Science. ⟨inria-00098618⟩
Accès au bibtex

ref_biblio: Guy-René Perrin, Dominique Méry (Dir.). RenPar'10. ULP, 264 p, 1998. ⟨inria-00098635⟩
Accès au bibtex

1993

Theses

ref_biblio: Dominique Méry. Une méthode de raffinement et de développement pour la programmation parallèle : econtribution à l'étude du raffinement de programmes parallèles : une approche fondée sur le concept de preuve. Autre. Université Henri Poincaré - Nancy 1, 1993. Français. ⟨NNT : 1993NAN10019⟩. ⟨tel-01753615⟩
Accès au bibtex