Gilles Bernot

Formal Methods for Software Engineering

INTERNATIONAL JOURNALS

M. Aiguier, J. Benzakki, G. Bernot, S. Beroff, D. Dupont, L. Freund, M. Israël, F. Rousseau, ECOS: A Generic Codesign Environment for the Prototyping of Real Time Applications, From Formal Specifications to Hardware-Software Partitioning .  Current Issues in Electronic Modeling (CIEM), Issue 8: Hardware/Software Co-Design & Co-Verification, J.M. Bergé, O. Levia, J. Rouillard eds., Kluwer Academic Publishers, Dordrecht, The Netherlands, p.23-57, ISBN 0-7923-9689-8 , 1996.

G. Bernot, M. Bidoit, T. Knapik, Observational specifications and the indistinguishability assumption .  Theoretical Computer Science (TCS), Vol.139, p.275-314, Elsevier Science Pub. B.V. (North-Holland) , 1995.
Also: LIENS Report 92-3, Ecole Normale Supérieure, Paris, France, 35 pages, January , 1992. [preliminary version]

G. Bernot, P. Le Gall, M. Aiguier, Label algebras and exception handling .  J. of Science of Computer Programming (SCP), Elsevier pub., Vol.23, num.2-3 p.227-286 , 1994.
Also: Shorter version in Chapter 6 of the "Diplôme d'habilitation à diriger des recherches en sciences" of Gilles Bernot, Université de Paris XI, Orsay, France, février , 1992. [preliminary version]

G. Bernot, M. Bidoit, T. Knapik, Observational approaches in algebraic specifications: A comparative study .  Acta Informatica, Vol.31, num.7, p.651-671 , 1994.
Also: LIENS Report 91-6, Ecole Normale Supérieure, Paris, France, April , 1991. [preliminary version]

G. Bernot, M.C. Gaudel, B. Marre, Software testing based on formal specifications: A theory and a tool .  Software Engineering Journal (SEJ), Vol.6, num.6, p.387-405 , 1991.
Also: LRI Report 581, Université de Paris XI, Orsay, France, June , 1990. [preliminary version]

G. Bernot, Correctness proofs for abstract implementations .  Information and Computation, Vol.80, num.2, p.121-151, Feb , 1989. [preliminary version]

G. Bernot, M. Bidoit, C. Choppy, Abstract data types with exception handling : an initial approach based on a distinction between exceptions and errors .  Theoretical Computer Science (TCS), Vol.46, num.1, p.13-45, Elsevier Science Pub. B.V. (North-Holland) , 1986.
Also: LRI Report 251, Université de Paris-Sud, Orsay, France, 48 pages, December , 1985.

NATIONAL JOURNALS

M.-C. Gaudel, B. Marre, F. Schlienger, G. Bernot, Les modèles de développement du logiciel .  Revue d'Électronique et d'Électrotechnique, Vol.6, p.34-40, juin , 1998.

BOOKS and BOOK CHAPTERS

M.C. Gaudel, G. Bernot, Algebraic Foundations of Systems Specification: The role of Formal Specifications .  Book Chapter I, IFIP State-of-the-Art Report on Algebraic Foundations of Systems Specification, E.Astesiano, H-J.Kreowski and B.Krieg-Bruckner Eds, p.1-12, Springer ISBN 3-540-63772-9, August , 1999. [preliminary version]

M. Aiguier, J. Benzakki, G. Bernot, S. Béroff, D. Dupont, L. Freund, M. Israël, F. Rousseau, ECOS : Environnement générique de cospécification .  CODESIGN conception conjointe logiciel-matèriel, CTI COMETE, Eyrolles, p.45-85, ISBN : 2-2120-5219-7 , 1998.

M-C. Gaudel, B. Marre, F. Schlienger, G. Bernot, Précis de génie logiciel .  Masson éditeur, Paris, collection Enseignement de l'Informatique, préface de Michel Lemoine, ISBN 2-225-85189-1, 142 pages , 1996.

M. Aiguier, G. Bernot, Algebraic semantics of object type specifications .  Book chapter in Information Systems Correctness and Reusability, Selected papers from the IS-CORE workshop, Amsterdam, Netherland, Sept. 1994, World Scientific Publishing, R.J.Wieringa & R.B.Feenstra eds, p.16-32 , 1995. [preliminary version]

REFEREED INTERNATIONAL CONFERENCES and WORKSHOPS

S. Coudert, G. Bernot, P. Le Gall, Hierarchical Heterogeneous Specifications .  Selected papers of the Intl Workshop on Abstract Data Types (WADT'98), Lisbon, Portugal. Recent Trends in Algebraic Development Techniques, J-L. Fiadeiro ed., Springer-Verlag LNCS 1589, p.107-121 , 1999. [preliminary version]

F. Mercier, A. Bertolino, P. Le Gall, G. Bernot, A systematic approach for integration testing of complex systems .  Proc. Proc. 11th Intl Conf. on Software Engineering and Its Applications, Vol.1, Session 6, Paris, France, December 8-10, , 1998. [link]

G. Bernot, L. Bouaziz, P. Le Gall, A Theory of Probabilistic Functional Testing .  Proc. of the Intl Conf. on Software Engineering (ICSE 97), p.216-226 , Boston, USA , 1997. [preliminary version]

M. Aiguier, G. Bernot, ETOILE-specifications: an Object Oriented Way of Specifying Systems .  Proc. of the Workshop on Proof Theory of Concurrent Object-Oriented Programming, Linz, Austria, p.50-57, J-P. Bahsoun, J. Fiadeiro, D. Galmiche, A. Yonezawa eds., 10th European Conf. on Object-Oriented Programming (ECOOP 96) , 1996. [preliminary version]

G. Bernot, S. Coudert, P. Le Gall, Towards heterogeneous formal specifications .  Proc. of the 5th Intl Conf on Algebraic Methodology And Software Technology (AMAST 96), Munich, Germany, Springer-Verlag LNCS 1101, p.458-472 , 1996.
Also: LIVE/LaMI Report 16-1995, Université d'Évry - Val d'Essonne, Évry, France, , 1995. [preliminary version]

M. Aiguier, S. Beroff, L. Freund, G. Bernot, M. Israël, Using Axiomatic Specifications for Hardware System Design .  Proc. of the 3rd Intl Conf on Concurrent Engineering & Electronic Design Automation (CEEDA'96), 18-19 January 1996, Poole, UK, in Managing Technology & Processes into the Next Millennium, S. Medhat & M. Bell eds, EPIC E.M. Publ, p.276-283 , 1996. [preliminary version]

M. Aiguier, J. Benzakki, G. Bernot, M. Israël, ECOS: from formal specification to hardware/software partitioning .  Proc. of the VHDL Forum'94, Grenoble, France , 1994. [abstract]

G. Bernot, P. Le Gall, Exception handling and term labelling .  Proc. of International Conference on Theory and Practice of Software Development (TAPSOFT), Orsay, France, Springer-Verlag LNCS 668, p.421-436 , 1993.
Also: LRI Report 712, Université de Paris XI, Orsay, France, December , 1991. [preliminary version]

G. Bernot, P. Le Gall, Label algebras: a systematic use of terms .  Selected papers of the 8th International Workshop on Abstract Data Types (WADT) joint with the 3rd COMPASS Workshop, Dourdan, 1991, France, Recent Trends in Data Type Specification, Springer-Verlag LNCS 655, p.144-163 , 1993.
Also: LRI Report 719, Université de Paris XI, Orsay, France, December , 1991. [preliminary version]

G. Bernot, M. Bidoit, T. Knapik, Towards an Adequate Notion of Observation .  Proc. of the 4th European Syposium on Programming (ESOP'92) Springer-Verlag LNCS 582, B. Krieg-Bruckner Ed., p.39-55, Rennes, France, February , 1992.
Also: LIENS Report 92-2, Ecole Normale Supérieure, Paris, France, January , 1992. [preliminary version]

G. Bernot, Testing against formal specifications: a theoretical view .  Proc. of the International Conference on Theory and Practice of Software Development (TAPSOFT'91 CCPSD), Brighton U.K., April 1991, Springer-Verlag LNCS 494, p.99-119 , 1991. [preliminary version]

G. Bernot, Good functors ... are those preserving philosophy ! .  Proc. of the Conference on Category Theory and Computer Science, Edimburgh, September 1987, Springer-Verlag LNCS 283, p.182-195 , 1987.
Also: Conférence invitée, Actes des journées ELIT 1988 - Esquisses, Logique et Informatique Théorique, juin - juillet 1988, organisateurs L.Coppey, C.Lair, M.Mathieu, volumes num.22 de DIAGRAMMES, Décembre , 1989. [preliminary version]

G. Bernot, M. Bidoit, C. Choppy, Algebraic semantics of exception handling .  Proc. of the European Symposium On Programming (ESOP'86), March 1986, Springer-Verlag LNCS 213, p.173-186 , 1986.
Also: LRI Report 257, Université de Paris XI, Orsay, France, 23 pages, January , 1986. [preliminary version]

G. Bernot, M. Bidoit, C. Choppy, Abstract implementations and correctness proofs .  Proc. of the 3rd Symposium on Theoretical Aspects of Computer Science (STACS), January 1986, Orsay, France, Springer-Verlag LNCS 210, B. Monien and G. Vidal-Naquet Ed., p.236-251 , 1986.
Also: LRI Report 250, Université de Paris XI, Orsay, France, 19 pages, December , 1985. [preliminary version]

INVITED INTERNATIONAL CONFERENCES and WORKSHOPS

G. Bernot, F. Klay, F. Ouabdesselam, The Feature Interaction Detection Method of VALISERV .  Invited talk, Joint ASPIRE / FIREworks Meeting, Evry, France, April 8-10 , 1999. [slides]

A. Arnoud, P. Le Gall, G. Bernot, Some aspects of Test Data Selection from Formal Specifications .  Invited talk, 1st Intl Software Quality Week Europe (QWE'97), Brussels, Belgium, 4-7 November , 1997. [preliminary version]

M. Aiguier, G. Bernot, Formal specifications for system design, and a proposal for object oriented extensions to VHDL .  Invited paper in Proc. of the First Workshop on Systems Design Languages, April 1997, San Jose, California , 1997.

S. Coudert, P. Le Gall, G. Bernot, An example of heterogeneous structured specification : a travel agency .  Invited talk, 12th Intl Workshop on Abstract Data Types (WADT'97), Tarquinia, Italy, June 1997 , 1997.
Also: Invited talk, ASPIRE Meeting, Lisbon, Portugal, September 19-20 , 1997.
Also: LaMI Report 28-1997, Université d'Évry, France , [preliminary version]

G. Bernot, ETOILE-Specifications and Real-Time issues .  Proc. of Dagstuhl seminar num.9715 on Object-Oriented Software Development, H.-D. Ehrich, Y. Feng, D. Kung eds, SchlossDagstuhl Report num.174, p.12-13, April , 1997. [preliminary version]

G. Bernot, Formal specifications in general, and some current research topics in algebraic specifications .  Invited paper in Proc. of the 6th Workshop on Knowledge Engineering Methods and Languages, KEML'96, Paris, France, January 1996, p.1-10 , 1996. [preliminary version]

G. Bernot, M. Aiguier, Object oriented algebraic specifications and the specification of systems .  Invited Intl Conf on Formal Specification: Foundations, Methods, Tools and Applications (FMTA'95), May 1995, Varsaw, Poland , 1995. [abstract]

G. Bernot, M. Aiguier, Algebraic specification of object types and systems .  Invited talk at the Joint Workshop on Abstract Data Types (WADT) and the COMPASS workshop, Sintra, Portugal, February , 1995.

M. Aiguier, G. Bernot, J. Ramos, A. Sernadas, An Algebraic Semantics for GNOME via a Translation to ÉTOILE Specifications .  Invited conference in Proc of the IS-CORE final Workshop, Évry, France, 7-9 September , 1995.
Also: Joint COMPASS workshop and WADT, Oslo, Norway, 19-23 September , 1995. [preliminary version]

G. Bernot, Formal specifications and algebraic specifications .  Invited paper in Proc. of the 7th International Software Quality Week, Software Research Institute Ed., San Francisco, California, USA, 17-20 Mai , 1994.
Also: LaMI Report 06-1994, Université d'Évry - Val d'Essonne, Évry, France, May , 1994. [preliminary version]

G. Bernot, Object oriented algebraic specifications and modularity issues .  Invited talk at the IS-CORE Workshop on Modularization, Orsay, April , 1994.

G. Bernot, E. David, On the usefulness of carriers, semi-initiality and semi-adjuncts for institution independent issues .  Invited paper in the 5th WADT/COMPASS Workshop, Santa Margherita, Italy, May/June , 1994.
Also: LIVE/LaMI Report 07-1994, Université d'Évry - Val d'Essonne, Évry, France , [preliminary version]

G. Bernot, M-C. Gaudel, P. Le Gall, B. Marre, Experience with Black-Box Testing from Formal Specification .  Invited paper, Proc. of the 2nd International Conference on Achieving Quality in Software (AQuIS'93), Venice, Italy, p.75-94, October , 1993.

G. Bernot, A theory of test selection from formal specifications .  Invited paper in Proc. of the ERCIM Workshop on Software Quality Principles and Techniques, May 1992, Pisa, Italy, p.153-172 , 1992. [preliminary version]

G. Bernot, M-C. Gaudel, B. Marre, A formal approach to software testing .  Invited paper in Proc. of the 2nd Intl Conf of Algebraic Methodology and Software Technology (AMAST-2), May 1991, Iowa City, USA. Workshops in Computing, Springer-Verlag , 1992. [preliminary version]

G. Bernot, M. Bidoit, Proving the correctness of algebraically specified software: Modularity and Observability issues .  Invited paper in Proc. of the 2nd Intl Conf of Algebraic Methodology and Software Technology (AMAST-2), May 1991, Iowa City, USA. Workshops in Computing, p.216-242, Springer-Verlag , 1992. [preliminary version] [extended version]

NATIONAL CONFERENCES and WORKSHOPS

G. Bernot, H. Jouve, F. Klay, F. Ouabdesselam, J-L. Richier, Aide à l'intégration de services par la génération de tests .  Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), p.9-20, Grenoble, 26-28 janvier , 2000. [preliminary version]

M Aiguier, J. Benzakki, G. Bernot, S. Beroff, D. Dupont, L. Freund, M. Israël, F. Rousseau, ECOS: un Environnement générique de CO-Spécification pour le prototypage d'applications temps réel, de la spécification formelle au partitionnement .  Actes des Séminaires Action Scientifique, Revue Codesign, France Telecom, No.10, p.65-74, Novembre , 1996. [preliminary version]

L. Bouaziz, G. Bernot, P. Le Gall, Probalistic Formula Testing .  Article invité aux Journées du GDR Programmation, Orléans, 20-22 novembre , 1996. [preliminary version]

M. Aiguier, G. Bernot, ETOILE-specifications: un formalisme algébrique de spécifications orientées objets .  Conférence invitée, Compte-rendu de la journée thématique Technologie Objet et Sureté de Fonctionnement, Groupe AFCET Technologie Objet, Saclay, 25 avril 1996, F. Terrier ed., Rapport DEIN/SLA/96-049, Centre d'Etudes de Saclay, INSTN-CEA , 1996.

G. Bernot, Spécifications formelles et test fonctionnel .  Conférence invitée aux journées AFCET "méthodes formelles", octobre 1993, LAAS, Toulouse , 1993.

P. Le Gall, G. Bernot, Algèbres étiquetées et traitement d'exception .  Journées GROPLAN et GRD Programmation et Outils de l'Intelligence Articielle, Nancy, mars , 1992.

PROJECT REPORTS

M. Aiguier, J. Benzakki, G. Bernot, S. Beroff, J.M. Delosme, D. Dupont, L. Freund, M. Israël, ECOS .  Rapport de fin de contrat, LaMI, Université d'Évry - Val d'Essonne, janvier , 1998.

M. Aiguier, J. Benzakki, G. Bernot, S. Beroff, L. Freund, M. Israël, ECOS .  Rapport de contrat à mi-parcours, LaMI, Université d'Évry - Val d'Essonne , 1996.

IS-CORE, Working Papers of the International Workshop on Information Systems - Correctness and Reusability. IS-CORE'95 .  Proc. of the IS-CORE'95 Workshop, Évry, France, G.Bernot and M.Aiguier editors, LIVE/LaMI Report 11-1995, Université d'Évry - Val d'Essonne, September , 1995.

G. Bernot, M.C. Gaudel, B. Marre, Le test statique de logiciel .  Rapport de fin de contrat Aérospatiale pour le CNES, avril 1994, centre commun de recherches Louis-Bleriot , 1994. [preliminary version]

G. Bernot, M.C. Gaudel, B. Marre, Etat de l'art et apport relatif des différentes techniques de test du logiciel .  Rapport de fin de contrat Aérospatiale DCR/Q 120488-91 pour le CNES, centre commun de recherches Louis-Bleriot, 55p , 1991. [preliminary version]

CGE / LRI / UoP METEOR teams, A Proposed List of Components for a Specification Development Environment .  ESPRIT project 432, METEOR/t11/CGE-LRI-UoP/SDE Report , 1987.

G. Bernot, P. Pauthe, IDEAS (Integrated Development Environment for Algebraic Specifications): a scenario .  ESPRIT project 432, METEOR/t11/BP/IDEAS Final Report , 1987.

SOME UNPUBLISHED RESEARCH REPORTS

P. Amar, G. Bernot, L'environnement générique pour spécifications formelles hétérogènes MSPEC .  Unpublished draft , 1999. [preliminary version]

S. Coudert, G. Bernot, P. Le Gall, General Structured Specifications .  Unpublished draft , 1996. [preliminary version]

A. Deo, P. Le Gall, G. Bernot, Semantics for algebraic specifications with iterators using polymorphic label algebras .  Unpublished draft , 1994.

A. Deo, P. Le Gall, G. Bernot, Introducing unbounded arities: sequence algebras .  LRI Report 938, Université de Paris XI, Orsay, France , 1994.

M. Aiguier, G. Bernot, P. Le Gall, An algebraic way to unequally treat equal values .  LIVE/LaMI Report 02-1993, Université d'Évry - Val d'Essonne, Évry, France , 1993. [preliminary version]

G. Bernot, B. Marre, Formal and Practical Aspects of Test Selection based on Algebraic Specifications .  LRI Report 560, Université de Paris-Sud, Orsay, France , 1990.

G. Bernot, A formalism for test with oracle based on algebraic specifications .  LIENS Report 89-4, Ecole Normale Supérieure, Paris, France , 1989.

G. Bernot, M. Bidoit, C. Choppy, Initial models of algebraic specifications with exception handling .  LRI Report 201, Orsay, France, 24 pages , 1984.

MEMOIRES

G. Bernot, Diplôme d'habilitation à diriger des recherches en sciences .  février 1992, LIENS (ENS Ulm) et Université de Paris-Sud, Orsay, France, 283 pages. Jury : G. Cousineau (président), E. Astesiano, M. Bidoit, M-C. Gaudel, J-P. Jouannaud, P. Lescanne, D. Sannella, G. Scollo , 1992. [full text]

G. Bernot, Une sémantique algébrique pour une spécification différenciée des exceptions et des erreurs : application à l'implémentation et aux primitives de structuration des spécifications formelles .  Thèse de troisième cycle en informatique, février 1986, LRI, Université de Paris-Sud, Orsay, France, 282 pages. Jury : J-P. Jouannaud (président), M-C. Gaudel & M. Bidoit & C. Choppy (directeurs), I. Guessarian, G. Vidal-Naquet , 1986. [full text]

G. Bernot, Implémentations de types abstraits algébriques en présence d'exceptions .  Rapport de DEA d'informatique, septembre 1984, LRI, Université de Paris-Sud, Orsay, France, 128 pages , 1984.

G. Bernot, Un théorème de connexité pour les variétés projectives .  Rapport de DEA de mathématiques pures, juin 1982, Laboratoire de mathématiques pures, Université de Paris-Sud, Orsay, France, 42 pages , 1982.