Aller au contenu
Trouver un autre spécialiste

Marc Frappier

Professeur, Faculté des sciences
FAC. SCIENCES Informatique

Présentation

Sujet de recherche

Software Development

Disciplines de recherche

Computer Science

Mots-clés

formal methods, Security, software engineering, software synthesis

Intérêts de recherche

Formal specification, design, verification, and testing of software using a multi-paradigm specification approach. Software synthesis. Security.

Langues parlées et écrites

Anglais, Français

Diplômes

(1995). (Doctorate, Ph.D.). University of Ottawa.

(1990). (Master's Thesis, Master - Masters). Université de Sherbrooke.

(1986). (Bachelor's, Bachelor). 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

  • Grant. (Awarded). Principal Investigator. Une approche formelle à la détection d’intrusion. Natural Sciences and Engineering Research Council of Canada (NSERC). subvention à la découverte. 168 000 $. (2019-2025)
  • Grant. (Awarded). Co-investigator. Sécurité dans l’Internet industriel des objets dans un contexte de connectivité 5G et de traitement en périphérie. Public Safety and Emergency Preparedness Canada (PSEPC). Programme de coopération en matière de cybersécurité (PCCS). 898 610 $. (2021-2024)
  • Grant. (Awarded). Principal Investigator. Évaluation de la résilience d’un redistributeur électrique dans un contexte d’industrie 4.0. Public Safety and Emergency Preparedness Canada (PSEPC). Programme de coopération en matière de cybersécurité. 1 054 171 $. (2020-2024)
  • Grant. (Awarded). Principal Investigator. Anomaly detection from system logs through deep learning. Mathematics of Information Technology and Complex Systems (MITACS). Accélération. 30 000 $. (2023-2023)
  • Grant. (Awarded). Principal Investigator. Cyberrésilience d’un redistributeur électrique dans un contexte d’industrie 4.0. Natural Resources Canada. Programme de la cybersécurité et de l’infrastructure énergétique essentielle. 376 050 $. (2020-2022)
  • Grant. (Awarded). Principal Investigator. Sécurité du standard MIL-STD-1553. Mathematics of Information Technology and Complex Systems (MITACS). Mitacs Accélération Exploration. 12 000 $. (2021-2021)
  • Grant. (Completed). Principal Investigator. 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)
  • Grant. (Awarded). Principal Investigator. Une approche formelle pour le contrôle d’accès et la gestion du consentement. Natural Sciences and Engineering Research Council of Canada (NSERC). 195 000 $. (2014-2019)
  • Grant. (Awarded). Principal Applicant. Stateful Intrusion Detection using Algebraic State-Transition Diagrams. Mathematics of Information Technology and Complex Systems (MITACS). Mitacs Accelerate Proposal. 15 000 $. (2018-2019)
  • Contract. (Completed). Principal Applicant. System modelling of the Nazareth/Bonaventure traffic management. Ville de Montréal. internal funding. 11 550 $. (2018-2018)
  • Grant. (Completed). Principal Applicant. Extending the ASTD interpreter with state variables. Communications Security Establishment (CSE Canada). internal funding. 11 000 $. (2018-2018)
  • Grant. (Completed). Principal Investigator. Methods and techniques for the automation and simplification of ICS honey pots deployments and monitoring. Natural Sciences and Engineering Research Council of Canada (NSERC). engage grant. 25 000 $. (2017-2017)
  • Grant. (Completed). Co-applicant. Centre de recherche sur les environnements intelligents. Fonds Institutionnel de Recherche de l'Université de Sherbrooke. PIFIR. 105 390 $. (2012-2015)
  • Contract. (Completed). Principal Investigator. Gestion du consentement. Centre Hospitalier de Sherbrooke. 342 000 $. (2012-2014)

Publications

Articles de revue

  • Mammar, M; Frappier, M; Laleau, R. (2024). An Event-B model of an automotive adaptive exterior light system. International Journal on Software Tools for Technology Transfer 26 331–346. DOI. (Published).
  • Mammar, M; Frappier, M. (2024). Modeling of a Speed Control System using Event-B. International Journal of Software Tools for Technology Transfer 26 347-363. DOI. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • Tidjon, L.*, Frappier, M., Leuschel, M., Mammar, A. (2019). Intrusion Detection Systems: A Cross-Domain Overview. IEEE Communication Surveys Tutorials 21 (4), 3639-3681. (Published).
  • 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. (Published).
  • Huynh, N.*, Frappier, M., Pooda, H.*, Mammar, A., Laleau. (2018). SGAC: a Multi-Layered Access Control Model with Conflict Resolution Strategy. The Computer Journal (Submitted).
  • 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 (Submitted).
  • 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. (In Press).
  • 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. (Published).
  • Frappier, M., Gervais, F., Laleau, R., Milhau, J*. (2014). Refinement Patterns for ASTD. Formal Aspects of Computing 26 (5), 919-941. (Published).
  • Benoît Fraikin*, Marc Frappier, Richard St-Denis. (2014). Supervisory Control Theory with Alloy. Science of Computer Programming 94 (part 2), 217-237. (Published).

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), (Published).

Articles de conférence

  • A. Soltani, D. Nkashama, J. Masakuna, M. Frappier, P. Tardif, F. Kabanza. (2024). Assessing Language Models for Semantic Textual Similarity in Cybersecurity. Lecture Notes in Computer Science (LNCS) 14828, 370-380. (Published).
  • D. Nkashama, J. Masakuna, A. Soltani, J.-C. Verdier, M. Frappier, P. Tardif, F. Kabanza. (2024). Deep Learning for Network Anomaly Detection under Data Contamination: Evaluating Robustness and Mitigating Performance Degradation. Lecture Notes in Computer Science (LNCS), 1-19. (In Press).
  • Fayçal Baba, Marc Frappier, Amel Mammar, Regine Laleau. (2024). Modeling and Verification of Solidity Smart Contracts with the B Method. Lecture Notes in Computer Science (LNCS) 14784, 1-20. (In Press).
  • Alex Rodrigue Ndouna, Marc Frappier. (2024). Modelling the mechanical lung ventilation system using TASTD. Lecture Notes in Computer Science (LNCS) 14759, 324-340. (Published).
  • J, M. Tshimula, D. K. Nkashama, P. Owusu, M. Frappier, P.-M. Tardif, F. Kabanza, A. Brun, J.-M. Patenaude, S. Wang, B. Chikhaoui. (2023). Characterizing Financial Market Coverage using Artificial Intelligence. arXiv.org, 1-12. (Published).
  • D. de Azevedo Oliveira, M. Frappier. (2023). Modelling an Automotive Software System with TASTD. Lecture Notes in Computer Science (LNCS) 14010, 124-141. (Published).
  • Cartellier, Q. Frappier, M. and Mammar, A. (2023). Proving Local Invariants in ASTDs. Lecture Notes in Computer Science (LNCS) 14308, 228-246. (Published).
  • D. de Azevedo Oliveira, M. Frappier. (2023). TASTD: a real-time extension for ASTD. Lecture Notes in Computer Science (LNCS) 14010, 142-159. (Published).
  • M. Alvarez, J.-C. Verdier, D. Kanda Nkashama, M. Frappier, P. M. Tardif, F. Kabanza. (2022). A Revealing Large-Scale Evaluation of Unsupervised Anomaly Detection Algorithms,. ML Evaluation Standards Workshop at ICLR 2022, 1-14. (Published).
  • C. El Jabri, M. Frappier, T. Ecarot, P. M. Tardif. (2022). Development of Monitoring Systems for Anomaly Detection Using ASTD Specifications. LNCS Lecture notes in computer science 13299, 274-289. (Published).
  • D. Kanda Nkashama, A. Soltani, J.-C. Verdier, M. Frappier, P. M. Tardif, F. Kabanza. (2022). Robustness Evaluation of Deep Unsupervised Learning Algorithms for Intrusion Detection Systems,. arXiv, 1-9. (Published).
  • J.-B. Larouche, S. Roy, F. Mailhot, P.-M. Tardif, M. Frappier. (2022). SCADA Radio Blackbox Reverse Engineering. Lecture Notes in Computer Science (LNCS) 13877, 287-302. (Published).
  • 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. (Published).
  • A. Mammar, M. Frappier and R. Laleau. (2020). An Event-B Model of an Automotive Adaptive Exterior Light System. Lecture Notes in Computer Science (LNCS) 12071, 351–366. (Published).
  • Lionel N. Tidjon, Marc Frappier, Amel Mammar. (2020). Intrusion Detection Using ASTDs. Advances in Intelligent Systems and Computing, vol 1151, 1397-1411. (Published).
  • A. Mammar, M. Frappier. (2020). Modeling a Speed Control System using Event-B. Lecture Notes in Computer Science (LNCS) 12071, 367–381. (Published).
  • D. de Azevedo Oliveira, M. Frappier. (2020). Verifying SGAC Access Control Policies: a Comparison of ProB, Alloy and Z3. Lecture Notes in Computer Science (LNC) 12071,, 223-229. (Published).
  • 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 - ICSOFT 2019, 170-177. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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, (Published).
  • 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. (Published).
  • Lionel Tidjon*, Marc Frappier, Michael Leuschel and Amel Mammar. (2018). Extended Algebraic State-Transition Diagrams. IEEE Computer Society, (Published).
  • 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. (In Press).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • Thomas Fayolle*, Marc Frappier, Régine Laleau , Frédéric Gervais. (2015). Formal refinement of extended state machines. arXiv.org, 1-16. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • 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. (Published).
  • Savary, A.*, Frappier, M., Lanet, J.-L. (2013). Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing. LNCS, 223-237. (Published).
  • 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. (Published).
  • Frappier, M., Mammar, A. (2012). An Assertions-Based Approach to Verifying the Absence Property Pattern. IEEE Computer Society, 361-370. (Published).
  • Fraikin, B.*, Frappier, M., St-Denis, R. (2012). Modeling the Supervisory Control Theory with Alloy. Springer Lecture Notes in Computer Science, 94-107. (Published).
  • Mammar, A., Frappier, M., Chane-Yack-Fa, R.*. (2012). Proving the Absence Property Pattern Using the B Method. IEEE Computer Society, 167-170. (Published).
  • Milhau, J.*, Gervais, F., Laleau, R., Frappier, M. (2012). Refinement Patterns for ASTD. ACM, 1-8. (Published).

Autres contributions

Gestion d'évènements

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

Activités de collaboration internationale

  • Collaborator. France. Collaborate with Pr Régine Laleau and Amel Mammar on the ANR research project FORMOSE, which aims to design a formally-grounded, model-based requirements engineering (RE) method for critical complex systems, supported by an open-source environment.

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, Japan
  • (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, Japan
  • (2016). Verification of security policies in access control. Implicit and explicit semantics integration in proof based developments of discrete systems. Shonan, Japan
  • (2013). Verification of infinite state ASTDs. Integration of Tools for Rigorous Software Construction and Analysis. Schloss Dagstuhl, Germany