Publications

Editeur invité :

• [GF11]  F. Gervais, B. Fraikin : Tool Building in Formal Methods – Extended Papers from WS-TBFM 2010. Software: Practice and Experience, Vol. 41, n°2, John Wiley & Sons, pp. 131-208, 2011.

Chapitre de livre :

• [GFS06]  F. Gervais, M. Frappier, R. St-Denis : EB³. In Software Specification Methods. Hermès Science Publishing, ISTE, ISBN : 1-905209-34-7, chapitre 14, pp. 259-274, 2006.

Revues internationales, avec comité de rédaction :

• [FGLM14] M. Frappier, F. Gervais, R. Laleau, J. Milhau : Refinement patterns for ASTDs. Formal Aspects of Computing, Vol. 26, n°5, pp. 919-941, Springer-Verlag, 2014.
  
• [EFGLS11c]  M. Embe Jiague, M. Frappier, F. Gervais, R. Laleau, R. St-Denis : Enforcing ASTD access-control policies with WS-BPEL processes in SOA environments. International Journal of Systems and Service-Oriented Engineering, Vol. 2, n° 2, pp. 37-59, IGI Publishing, 2011.
• [GFL09]  F. Gervais, M. Frappier, R. Laleau : Generating relational database transactions from EB³ attribute definitions. Software and Systems Modeling, Vol. 8, n° 3, pp. 423-445, Springer-Verlag, 2009.
• [FGLFS08]  M. Frappier, F. Gervais, R. Laleau, B. Fraikin, R. St-Denis : Extending Statecharts with process algebra operators. Innovations in Systems and Software Engineering, Vol. 4, n° 3, pp. 285-292, Springer-Verlag, 2008.

Revue nationale, avec comité de rédaction :

• [Ger07]  F. Gervais : EB⁴, vers une méthode de spécification formelle des SI. Ingénierie des Systèmes d’Information, Vol. 12, n° 4, pp. 69-93, Hermès, 2007.

Conférences internationales, avec comité de sélection et actes :

• [CG23] J. Cervelle, F. Gervais : Introducing inductive construction in B with the Theory Plugin. In 9th International Conference on rigorous state based methods (ABZ 2023), Nancy, France, 30 May – 2 June. Springer, LNCS 14010, pp. 43-58, 2023.
• [FFGL16] T. Fayolle, M. Frappier, F. Gervais, R. Laleau : Modelling a hemodialysis machine using algebraic state-transition diagrams and B-like methods. In 5th International ABZ Conference (ABZ 2016), Linz, Austria, 23-27 May. Springer-Verlag, LNCS 9675, pp. 394-408, 2016.
• [EFGKLMS11]  M. Embe Jiague, M. Frappier, F. Gervais, P. Konopacki, R. Laleau, J. Milhau, R. St-Denis : A four-concern-oriented secure IS development approach. In 8th International Joint Conference on e-Business and Telecommunications (ICETE 2011), Sevilla, Spain, 18-21 July. INSTICC Press, volume SECRYPT 2011, pp. 464-471, 2011.
• [MGL11b]  A. Matoussi, F. Gervais, R. Laleau : A goal-based approach to guide the design of an abstract Event-B specification. In 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2011), Las Vegas, Nevada, USA, 27-29 April. IEEE Computer Society Press, pp. 139-148, 2011.
• [MFGL10]  J. Milhau, M. Frappier, F. Gervais, R. Laleau : Systematic translation rules from ASTD to Event-B. In 8th International Conference on Integrated Formal Methods (IFM 2010), Nancy, France, 12-14 October. Springer-Verlag, LNCS 6396, pp. 245-259, 2010.
• [EFGKLMS10]  M. Embe Jiague, M. Frappier, F. Gervais, P. Konopacki, R. Laleau, J. Milhau, R. St-Denis : Model-driven engineering of functional security policies. In 12th International Conference on Enterprise Information Systems (ICEIS 2010), Funchal, Madeira, Portugal, 8-12 June. INSTICC Press, volume Information Systems Analysis and Specification, pp. 374–379, 2010.
• [FFGLR07]  M. Frappier, B. Fraikin, F. Gervais, R. Laleau, M. Richard : Synthesizing information systems: the APIS project. In 1st International Conference on Research Challenges in Information Science (RCIS 2007), Ouarzazate, Morocco, 23-26 April. C. Rolland, O. Pastor, J.-L. Cavarero (éditeurs), pp. 73-84, 2007.
• [GFL07a]  F. Gervais, M. Frappier, R. Laleau : Refinement of EB³ process patterns into B specifications. In 7th International B Conference (B 2007), Besançon, France, 17-19 January. Springer-Verlag, LNCS 4355, pp. 201-215, 2007.
• [GBFL06b]  F. Gervais, P. Batanado, M. Frappier, R. Laleau : EB³TG: A tool synthesizing relational database transactions from EB³ attribute definitions. In 8th International Conference on Enterprise Information Systems (ICEIS 2006), Paphos, Cyprus, 24-27 May. INSTICC Press, Volume Information Systems Analysis and Specification, pp. 44-51, 2006.
• [GFL05d]  F. Gervais, M. Frappier, R. Laleau : Synthesizing B specifications from EB³ attribute definitions. In 5th International Conference on Integrated Formal Methods (IFM 2005), Eindhoven, The Netherlands, 29 November – 2 December. Springer-Verlag, LNCS 3771, pp. 207-226, 2005.
• [GFL05c]  F. Gervais, M. Frappier, R. Laleau : Generating relational database transactions from recursive functions defined on EB³ traces. In 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany, 7-9 September. IEEE Computer Society Press, pp. 117-126, 2005.
• [BGL03b]  S. Blazy, F. Gervais, R. Laleau : Reuse of specification patterns with the B method. In 3rd International Conference of B and Z Users (ZB 2003), Turku, Finland, 4-6 June. Springer-Verlag,LNCS 2651, pp. 40-57, 2003.

Workshops internationaux, avec comité de sélection et actes :

• [FFGL15] T. Fayolle, M. Frappier, F. Gervais, R. Laleau : Formal refinement of extended state machines. In 17th Refinement Workshop (REFINE 2015), Oslo, Norway, 22 June 2015. EPTCS 209, pp. 1-16, 2016.
• [MGLF12] J. Milhau, F. Gervais, R. Laleau, M. Frappier : Refinement patterns for ASTD. In 5th International Workshop UML and Formal Methods (UML&FM 2012), Paris, France, 27 Août. ACM SIGSOFT Software Engineering Notes, volume 37, numéro 4, pp. 1-8, 2012.
• [EFGLS11b]  M. Embe Jiague, M. Frappier, F. Gervais, R. Laleau, R. St-Denis : A metamodel for the design of access-control policy enforcement managers: work in progress. In 4th MITACS Workshop on Foundations & Practice of Security (FPS 2011), Paris, France, 12-13 Mai. Springer-Verlag, LNCS 6888, pp. 218-226, 2011.
• [EFGLS11a]  M. Embe Jiague, M. Frappier, F. Gervais, R. Laleau, R. St-Denis : From ASTD access control policies to WS-BPEL processes deployed in a SOA environment. In 1st International Symposium on Web Intelligent Systems & Services (WISS 2010), Hong Kong, Chine, 12-14 Décembre 2010. Springer-Verlag, LNCS 6724, pp. 126-141, 2011.
• [MGL11a]  A. Matoussi, F. Gervais, R. Laleau : Specification of a localization component driven by a goal-based approach: some lessons we learned. In 13th Brazilian Symposium on Formal Methods (SBMF 2010), Natal, Rio Grande do Norte, Brazil, 8-12 Novembre 2010. Springer-Verlag, LNCS 6527, pp. 177-193, 2011.
• [GFL05b]  F. Gervais, M. Frappier, R. Laleau : How to synthesize relational database transactions from EB³ attribute definitions? In 3rd International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2005), Miami, USA, 24-25 Mai. INSTICC Press, pp. 83-88, 2005.

Conférences nationales, avec comité de sélection et actes :

• [SMFFGL10]  K. Salabert, J. Milhau, B. Fraikin, M. Frappier, F. Gervais, and R. Laleau : iASTD : un interpréteur pour les ASTD, In Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2010), Poitiers, France, 9-11 Juin. Actes AFADL, pp. 3-6, 2010.
• [MGL09]  A. Matoussi, F. Gervais, R. Laleau : De KAOS vers Event-B : approche dirigée par les buts. In Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2009), Toulouse, France, 26-28 Janvier. Actes AFADL, pp. 71–86, 2009.
• [Ger06a]  F. Gervais : EB⁴ : Vers une méthode de spécification formelle des SI. In 24ème Congrès INFORSID, Hammamet, Tunisie, 1-3 Juin. INFORSID, Volume II, pp. 561-576, 2006.
• [MGL06b]  A. Mammar, F. Gervais, R. Laleau : Systematic identification of preconditions from set-based integrity constraints. In 24ème Congrès INFORSID, Hammamet, Tunisie, 1-3 Juin. INFORSID, Volume II, pp. 595-610, 2006.
• [GBFL06a]  F. Gervais, P. Batanado, M. Frappier, R. Laleau : Génération automatique de transactions de base de données relationnelle à partir de définitions d’attributs EB³. In Atelier Approches Formelles dans l’Assistance au Développement du Logiciel (AFADL 2006), Paris, France, 15-17 Mars. Rapport ENST S 002, pp. 25-39, 2006.

Workshops nationaux, avec sélection sur la base d’un résumé :

• [BGFL06]  P. Batanado, F. Gervais, M. Frappier, R. Laleau : EB³TG : Un outil de génération de transactions de base de données relationnelle pour EB³. Session Outils de l’Atelier AFADL 2006, Paris, France, 15-17 Mars 2006.
• [BGL03a]  S. Blazy, F. Gervais, R. Laleau : Une démarche outillée pour spécifier formellement des patrons de conception réutilisables. In Workshop Objets, Composants et Modèles dans l’Ingénierie des SI (OCM-SI 2003), Nancy, France, 3 Juin. INFORSID, pp. 5-9, 2003.

Communications :

• [Ger16]  F. Gervais : Enquête auprès des adhérents de la SIF. Article, bulletin 1024, numéro 8, pp. 19-24, 2016.
• [MGV10]  D. Michel, F. Gervais, P. Valarcher : B-ASM: Specification of ASM à la B. Papier court, conférence ABZ 2010, Orford, Québec, Canada, 23-25 Février 2010.
• [MGL08]  A. Matoussi, F. Gervais, R. Laleau : A First Attempt to Express KAOS Refinement Patterns with Event B. Papier court, conférence ABZ 2008, Londres, Royaume-Uni, 16-18 Septembre 2008.
• [Ger05]  F. Gervais : EB⁴: Towards an integrated formal method for specifying information systems. Session poster ZB2005, Guildford, Royaume-Uni, 14 Avril 2005.

Rapports techniques :

• [FGLF08] M. Frappier, F. Gervais, R. Laleau, B. Fraikin : Algebraic state transition diagrams. Rapport technique n. 24, GRIL, Département d’informatique, Université de Sherbrooke (Québec), Canada, Juin 2008.
• [GFL07b]  F. Gervais, M. Frappier, R. Laleau : Comparing different combinations of event-based and state-based specifications for IS modelling. Rapport technique n. 18, GRIL, Département d’informatique, Université de Sherbrooke (Québec), Canada, Avril 2007.
• [MGL06a]  A. Mammar, F. Gervais, R. Laleau : Generating B preconditions from typical IS invariants. Rapport technique, LASSY, Université du Luxembourg, Luxembourg, Février 2006.
• [GFL05a]  F. Gervais, M. Frappier, R. Laleau : Vous avez dit raffinement ? Rapport technique n. 829, CEDRIC, CNAM-IIE, Evry, France, Mars 2005.
• [GFLB05]  F. Gervais, M. Frappier, R. Laleau, P. Batanado : EB³ attribute definitions: Formal language and application. Rapport technique n. 700, CEDRIC, CNAM-IIE, Evry, France, Février 2005.
• [GFL04]  F. Gervais, M. Frappier, R. Laleau : Synthesizing B substitutions for EB³ attribute definitions. Rapport technique n. 683, CEDRIC, CNAM-IIE, Evry, France, Novembre 2004.
• [BGL02]  S. Blazy, F. Gervais, R. Laleau : Un exemple de réutilisation de patterns de spécification avec la méthode B. Rapport technique n. 395, CEDRIC, CNAM-IIE, Evry, France, Novembre 2002.

Thèse et mémoires :

• [Ger06b]  F. Gervais : Combinaison de spécifications formelles pour la modélisation des systèmes d’information. Thèse de doctorat, spécialité informatique, CNAM Paris, Université de Sherbrooke (Québec), Décembre 2006.
• [Ger04]  F. Gervais : EB⁴ : Vers une méthode combinée de spécification formelle des systèmes d’information. Examen de spécialité, Doctorat Informatique, Université de Sherbrooke (Québec), Canada, Juin 2004.
• [Ger02]  F. Gervais : Réutilisation de composants de spécification en B. Mémoire de DEA, DEA Informatique, Université d’Evry Val d’Essonne, Evry, France, Juillet 2002. Stage réalisé au CEDRIC, IIE, Evry, France, Février-Juillet 2002.
• [Ger01]  F. Gervais : Etude des phénomènes d’hysteresis : Identification des paramètres du modèle de Bouc Wen et analyse des résultats. Mémoire de DEA, DEA Analyse et Systèmes Aléatoires, Université de Marne-la-Vallée, Champs-sur-Marne, France, Septembre 2001. Stage réalisé au LAMI, ENPC, Champs-sur-Marne, France, Avril-Septembre 2001.