Aller au contenu
Trouver un autre spécialiste

Marc Frappier

Professeur, Faculté des sciences
FAC. SCIENCES Informatique

Présentation

Sujet de recherche

Développement de logiciels

Disciplines de recherche

Informatique

Mots-clés

génie logiciel, méthodes formelles, Sécurité, synthèse automatique de logiciel

Intérêts de recherche

Spécification formelle, conception, vérification et test de logiciels en utilisant une approche de spécification multiparadigme (méthode B, state machine, process algebra). Sécurité et contrôle d'accès.

Langues parlées et écrites

Anglais, Français

Diplômes

(1995). (Doctorat, Ph. D.). Université d'Ottawa.

(1990). (Maîtrise avec mémoire, Maîtrise - Maîtrise). Université de Sherbrooke.

(1986). (Baccalauréat, Baccalauréat). Université de Sherbrooke.

Expérience académique

Professeur titulaire. (2005-). Université de Sherbrooke. Canada.

Professeur invité. (2019-2019).

invited professor. (2016-2016).

Invited professor. (2013-2013).

Invited professor. (2009-2009).

Invited professor. (2006-2006).

Professeur aggrégé. (1998-2005). Université de Sherbrooke. Canada.

invited professor. (1999-2003).

professeur adjoint. (1995-1998). Université de Sherbrooke. Canada.

Prix et distinctions

  • Distinguished Service Award 2019. Cs-Can | Info-Can. (Distinction).

Financement

  • Subvention. (Obtenu). Chercheur principal. Évaluation de la résilience d’un redistributeur électrique dans un contexte d’industrie 4.0. Sécurité Publique et Protection Civile du Canada (SPPCC). Programme de coopération en matière de cybersécurité. 1 054 171 $. (2020-2024)
  • Subvention. (Obtenu). Chercheur principal. Cyberrésilience d’un redistributeur électrique dans un contexte d’industrie 4.0. Ressources naturelles Canada. Programme de la cybersécurité et de l’infrastructure énergétique essentielle. 376 050 $. (2020-2022)
  • Subvention. (Obtenu). Chercheur principal. Sécurité du standard MIL-STD-1553. Mathematics of Information Technology and Complex Systems (MITACS). Mitacs Accélération Exploration. 12 000 $. (2021-2021)
  • Subvention. (Terminé). Chercheur principal. Apprentissage automatique de paramètres de règles de sécurité pour OfficeProtect. Mathematics of Information Technology and Complex Systems (MITACS). Accélération. 30 000 $. (2019-2019)
  • Subvention. (Obtenu). Chercheur principal. Une approche formelle pour le contrôle d’accès et la gestion du consentement. Conseil de Recherches en Sciences Naturelles et Génie du Canada (CRSNG). 195 000 $. (2014-2019)
  • Subvention. (Obtenu). Candidat principal. Stateful Intrusion Detection using Algebraic State-Transition Diagrams. Mathematics of Information Technology and Complex Systems (MITACS). Mitacs Accelerate Proposal. 15 000 $. (2018-2019)
  • Contrat. (Terminé). Candidat principal. System modelling of the Nazareth/Bonaventure traffic management. Ville de Montréal. internal funding. 11 550 $. (2018-2018)
  • Subvention. (Terminé). Candidat principal. Extending the ASTD interpreter with state variables. Communications Security Establishment (CSE Canada). internal funding. 11 000 $. (2018-2018)
  • Subvention. (Terminé). Chercheur principal. Methods and techniques for the automation and simplification of ICS honey pots deployments and monitoring. Conseil de Recherches en Sciences Naturelles et Génie du Canada (CRSNG). engage grant. 25 000 $. (2017-2017)
  • Subvention. (Terminé). Cocandidat. Centre de recherche sur les environnements intelligents. Fonds Institutionnel de Recherche de l'Université de Sherbrooke. PIFIR. 105 390 $. (2012-2015)
  • Contrat. (Terminé). Chercheur principal. Gestion du consentement. Centre Hospitalier de Sherbrooke. 342 000 $. (2012-2014)

Publications

Articles de revue

  • Mammar, A., Frappier, M., Laleau, R., Tueno Fotso, S.J. (2020). A formal refinement-based analysis of the hybrid ERTMS/ETCS level 3 standard. Journal of Software Tools for Technology Transfer 22 (3), 333–347. (Article publié).
  • Tueno Fotso, S.J., Frappier, M. Mammar, A., Laleau, R. (2020). Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach. Journal of Software Tools for Technology Transfer 22 (3), 349–363. (Article publié).
  • Sebastian Krings, Michael Leuschel, Joshua Schmidt,David Schneider,Marc Frappier. (2020). Translating Alloy and Extensions to Classical B. Science of computer programming 188 (1), 1-25. (Article publié).
  • Tidjon, L.*, Frappier, M., Leuschel, M., Mammar, A. (2019). Intrusion Detection Systems: A Cross-Domain Overview. IEEE Communication Surveys Tutorials 21 (4), 3639-3681. (Article publié).
  • Chane-Yack-Fa R*, Frappier M, Mammar A, Finkel A. (2018). Parameterized verification of monotone information systems. Formal Aspects of Computing 30 (3), 463–489. (Article publié).
  • Huynh, N.*, Frappier, M., Pooda, H.*, Mammar, A., Laleau. (2018). SGAC: a Multi-Layered Access Control Model with Conflict Resolution Strategy. The Computer Journal (Article soumis).
  • Tueno Fotso S.J.*, Frappier, M., Laleau, R. Mammar, A. (2018). Translation Rules from Ontology-based Domain Models to B System Specifications. Information and Software Technology (Article soumis).
  • Nghi Huynh*, Marc Frappier, Amel Mammar, Régine Laleau, Jules Desharnais. (2016). A Formal Validation of the RBAC ANSI 2012 Standard using B. Science of Computer Programming 1-18. (Article sous presse).
  • Mammar, Amel, Frappier, Marc. (2015). Proof-Based Verification Approaches for Dynamic Properties: Application to the Information System Domain. Formal Aspects of Computing 27 (2), 335-374. (Article publié).
  • Frappier, M., Gervais, F., Laleau, R., Milhau, J*. (2014). Refinement Patterns for ASTD. Formal Aspects of Computing 26 (5), 919-941. (Article publié).
  • Benoît Fraikin*, Marc Frappier, Richard St-Denis. (2014). Supervisory Control Theory with Alloy. Science of Computer Programming 94 (part 2), 217-237. (Article publié).

Numéros de revue

  • Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves. (2013). Abstract State Machines, Alloy, B and Z Selected papers from ABZ 2010. Science of Computer Programming (78), (Article publié).

Articles de conférence

  • Létourneau, L.-S., El Jabri, C., Frappier, M., Tardif, P.-M., Lépine, G., Boisvert, G. (2021). Statistical Approach For Cloud Security: Microsoft Office 365 audit logs case study. IEEE, 15-18. (Article publié).
  • A. Mammar, M. Frappier and R. Laleau. (2020). An Event-B Model of an Automotive Adaptive Exterior Light System. Rigorous State-Based Methods - 7th International Conference. 351–366. (Article publié).
  • Lionel N. Tidjon, Marc Frappier, Amel Mammar. (2020). Intrusion Detection Using ASTDs. Advanced Information Networking and Applications 2020. 1397-1411. (Article publié).
  • A. Mammar, M. Frappier. (2020). Modeling a Speed Control System using Event-B. Rigorous State-Based Methods - 7th International Conference. 367–381. (Article publié).
  • D. de Azevedo Oliveira, M. Frappier. (2020). Verifying SGAC Access Control Policies: a Comparison of ProB, Alloy and Z3. Rigorous State-Based Methods - 7th International Conference. 223-229. (Article publié).
  • Tueno Fotso, S.J., Laleau, R., Barradas, H.R., Frappier, M., Mammar, A. (2019). A Formal Requirements Modeling Approach: Application to Rail Communication. International Conference on Software Technologies. 170-177. (Article publié).
  • Krings S, Schmidt J, Brings C, Frappier M, Leuschel M. (2018). A Translation from Alloy to B. Abstract State Machines, Alloy, B and Z, 6th International Conference (ABZ 2018), 71-86. (Article publié).
  • Mammar A, Frappier M, Laleau R, Tueno Fotso S.J.*. (2018). An Event-B Model of the Hybrid ERTMS/ETCS Level 3 Standard, Abstract State Machines. Abstract State Machines, Alloy, B and Z, 6th International Conference (ABZ 2018), 353-366. (Article publié).
  • Tueno Fotso Steve Jeffrey*, Marc Frappier, Regine Laleau and Amel Mammar. (2018). Back Propagating B System Updates on SysML/KAOS Domain Models. IEEE Computer Society, (Article publié).
  • Tueno Fotso S.J.*, Mammar A, Laleau R, Frappier M. (2018). Event-B Expression and Validation of Translation Rules Between SysML/KAOS Domain Models and B System Specifications. Abstract State Machines, Alloy, B and Z, 6th International Conference (ABZ 2018), 55-70. (Article publié).
  • Lionel Tidjon*, Marc Frappier, Michael Leuschel and Amel Mammar. (2018). Extended Algebraic State-Transition Diagrams. IEEE Computer Society, (Article publié).
  • Tueno Fotso S.J.*, Frappier M, Laleau R, Mammar A, Leuschel M. (2018). Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions. International Conference on Integrated Formal Methods (IFM2018), 1-20. (Article sous presse).
  • Tueno Fotso S.J.*, Frappier M., Mammar A, Laleau R. (2018). Modelling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach. Abstract State Machines, Alloy, B and Z, 6th International Conference (ABZ 2018), 262-276. (Article publié).
  • Kenfack Ngankam H.*, Pigot H, Frappier M, Oliveira C, Giroux S. (2017). Formal Specification for Ambient Assisted Living Scenarios. 11th International Conference on Ubiquitous Computing and Ambient ?Intelligence (UCAmI), 508-519. (Article publié).
  • Tueno Fotso SJ*, Laleau R, Mammar A, Frappier M. (2017). Towards Using Ontologies for Domain Modelling within the SysML/KAOS Approach. 7th International Workshop on Model-Driven Requirements Engineering (MoDRE), 1-5. (Article publié).
  • Huynh N*, Frappier M, Mammar A, Laleau R. (2017). Verification of SGAC Access Control Policies using Alloy and ProB. 18th IEEE International Symposium on High Assurance Systems Engineering (HASE), 120-123. (Article publié).
  • Nghi Huynh* ; Marc Frappier ; Herman Pooda* ; Amel Mammar ; Régine Laleau. (2016). A Patient-Centered Access Control Method. 10th IEEE International Conference on Research Challenges in Information Science (RCIS), 1-12. (Article publié).
  • Thomas Fayolle*, Marc Frappier , Frédéric Gervais, Régine Laleau. (2016). Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods. Abstract State Machines, Alloy, B and Z, 5th International Conference (ABZ 2016), 394-408. (Article publié).
  • Thomas Fayolle*, Marc Frappier, Régine Laleau , Frédéric Gervais. (2015). Formal refinement of extended state machines. arXiv.org, 1-16. (Article publié).
  • Aymerick Savary*, Marc Frappier , Michael Leuschel, Jean-Louis Lanet. (2015). Model-Based Robustness Testing in Event-B Using Mutation. 13th International Conference on Software Engineering and Formal Methods (SEFM 2015), 132-147. (Article publié).
  • Fama Diagne*, Amel Mammar, Marc Frappier. (2014). A Tool for Verifying Dynamic Properrties in B. 12th International Conference on Software Engineering and Formal Methods (SEFM 2014), 290-295. (Article publié).
  • Nghi Huynh*, Marc Frappier, Amel Mammar, Régine Laleau, Jules Desharnais. (2014). Validating the RBAC ANSI 2012 Standard using B. Abstract State Machines, Alloy, B and Z, 4th International Conference (ABZ 2014), 255-270. (Article publié).
  • Amel Mammar, Marc Frappier. (2014). Verifying the Precedence Property Pattern Using the B Method. 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), 229 - 233. (Article publié).
  • Savary, A.*, Frappier, M., Lanet, J.-L. (2013). Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing. LNCS, 223-237. (Article publié).
  • Ferrier-Belhaouari, H., Konopacki, P.*, Laleau, R., Frappier, M. (2012). A Design by Contract Approach to Verify Access Control Policies. IEEE Computer Society, 263-272. (Article publié).
  • Frappier, M., Mammar, A. (2012). An Assertions-Based Approach to Verifying the Absence Property Pattern. IEEE Computer Society, 361-370. (Article publié).
  • Fraikin, B.*, Frappier, M., St-Denis, R. (2012). Modeling the Supervisory Control Theory with Alloy. Springer Lecture Notes in Computer Science, 94-107. (Article publié).
  • Mammar, A., Frappier, M., Chane-Yack-Fa, R.*. (2012). Proving the Absence Property Pattern Using the B Method. IEEE Computer Society, 167-170. (Article publié).
  • Milhau, J.*, Gervais, F., Laleau, R., Frappier, M. (2012). Refinement Patterns for ASTD. ACM, 1-8. (Article publié).

Autres contributions

Gestion d'évènements

  • pc member. (2021) Formal Requirements 2021. (Conférence).
  • pc member. (2021) 8th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z,. (Conférence).
  • pc member. (2021) International Conference On Formal Methods In Software Engineering FORMALISE 2021. (Conférence).
  • pc member. (2020) 16th International Conference on integrated Formal Methods (iFM2020). (Conférence).
  • pc member. (2020) The 22nd International Conference on Formal Engineering Methods ICFEM 2020. (Conférence).
  • pc member. (2020) SAM2020 - Languages, Methods, and Tools for AI-based Systems. (Conférence).
  • pc member. (2020) Formal Requirements 2020. (Conférence).
  • pc member. (2020) 7th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z,. (Conférence).
  • pc member. (2020) International Conference On Formal Methods In Software Engineering FORMALISE 2020. (Conférence).
  • pc member. (2019) The 21st International Conference on Formal Engineering Methods ICFEM 2019. (Conférence).
  • PC member. (2019) Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). (Conférence).
  • pc member. (2019) Formal Requirements 2019. (Conférence).
  • pc member. (2019) 7th Conference on Formal Methods in Software Engineering, FormaliSE 2019. (Conférence).
  • PC Member. (2018) 20th International Conference on Formal Engineering Methods (ICFEM 2018). (Conférence).
  • PC Member. (2018) 12th International Conference on Verification and Evaluation of Computer and Communication Systems. (Conférence).
  • pc member. (2018) 12th International Conference on Verification and Evaluation of Computer and Communication Systems vecos2018. (Conférence).
  • PC Member. (2018) 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 2018. (Conférence).
  • pc member. (2017) 11th International Conference on Verification and Evaluation of Computer and Communication Systems vecos 2017. (Conférence).
  • pc member. (2017) 18th IEEE International Symposium on High Assurance Systems Engineering (HASE 2017). (Conférence).
  • PC member. (2016) Abstract State Machines, Alloy, B and Z, 5th International Conference (ABZ 2016). (Conférence).
  • pc member. (2016) 17th IEEE International Symposium on High Assurance Systems Engineering (HASE). (Conférence).
  • pc member. (2015) 13th International Conference on Software Engineering and Formal Methods. (Conférence).
  • PC Member. (2014) 12th International Conference on Software Engineering and Formal Methods. (Conférence).
  • PC Member. (2014) 4th ABZ International Conference (ABZ 2014). (Conférence).
  • PC Member. (2014) 14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014). (Conférence).
  • PC Member. (2013) 3rd International Workshop on Information Systems Security Engineering WISSE’13. (Conférence).
  • PC Member. (2012) 5TH INTERNATIONAL SYMPOSIUM ON FOUNDATIONS & PRACTICE OF SECURITY. (Conférence).
  • PC Member. (2012) 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13). (Conférence).
  • PC Member. (2012) 2nd International Workshop on Information Systems Security Engineering WISSE’12. (Conférence).
  • PC member. (2012) Abstract State Machines, Alloy, B, VDM and Z, Third International Conference, ABZ 2012. (Conférence).

Activités de collaboration internationale

  • Collaborator. France. Collaboration with professors Régine Laleau (Université Paris-Est Créteil) et Amel Mammar (Télécom Sud Pais) on the ANR project FORMOSE, whose objective is to design a formally-grounded, model-based requirements engineering (RE) method for critical complex systems, supported by an open-source environment. The main partners are: ClearSy, LACL, Institut Mines-Telecom, OpenFlexo, and THALES.

Présentations

  • (2019). Security with SGAC and ASTDs. Invited seminar. Toulouse, France
  • (2018). Algebraic State-Transition Diagrams. Journées nationales du GDR GPL, 12-15 Juin 2018. Grenoble, France
  • (2018). The A720-A10 Interchange Case Study in SysML/KAOS. Shonan Seminar 121, Towards industrial application of advanced formal methods for cyber-physical system engineering, Shonan Village Center, Japan, November 5–8, 2018. Shonan village center, Japon
  • (2016). Evaluation and comparaison of access control models. Telecom SudParis. Évry, France
  • (2016). Generating Vulnerability Tests for Java Card Structural Constraints. Event-B Day, National Institute of Informatics (National Center of Sciences). Tokyo, Japon
  • (2016). Verification of security policies in access control. Implicit and explicit semantics integration in proof based developments of discrete systems. Shonan, Japon
  • (2013). Verification of infinite state ASTDs. Integration of Tools for Rigorous Software Construction and Analysis. Schloss Dagstuhl, Allemagne