Research Work
In this page, you will find an overview of the work I am doing and have done.
Main Topics
My main topics include the following points:
- Heterogeneous (hybrid, cyber-physical) systems
- Logic and proof, co-verification
- State-based formal methods
- Abstract state machines, Event-B, refinement-based approaches
- Model-driven engineering, software design
Formal Methods for Cyber-Physical Systems
Cyber-Physical Systems, as coined by Edward Lee, is a category of systems that incorporate discrete and continuous behaviours, as well as notions of network and autonomy.
The hybrid nature of CPS make them quite hard to verify; in particular, classical formal methods are particularly efficient for discrete aspects, while control theory is better suited for continuous features, but we lack something in-between, that makes the link between discrete and continuous.
In the context of my thesis, in particular, I took interest in modelling hybrid and cyber-physical systems using the Event-B formal method, together with its extension mechanism (theories).
The resulting contribution is a set of formalisms, theories, generic models and formal patterns, that together form a generic framework for hybrid system design.
This topic has been my main research topic in the last 4 years, and is the subject my Ph.D. thesis at IRIT-ENSEEIHT, supervised by Pr. Yamine Aït-Ameur, Dr. Neeraj K. Singh and Dr. Marc Pantel. It falls within the DISCONT ANR project, as well as within the main topics of the ACADIE team.
Publications
Here is a (reasonably up-to-date) list of my publications, in descending chronological order.
The models associated to these publications can be found here.
Thesis
The full manuscript of my thesis is available here.
Conference Papers
- Event-B Refinement for Continuous Behaviours Approximation, In 19th International Symposium on Automated Technology for Verificaiton and Analysis, ATVA 2021, 2021
- An Event-B Based Generic Framework for Hybrid Systems Formal Modelling, In 16th International Conference on integarted Formal Methods, iFM 2020, November 16-20, 2020, (LNCS 12546) [link] [video]
- Embedding Approximation in Event-B: Safe Hybrid System Design using Proof and Refinement, In 22nd International Conference on Formal Engineering Methods, ICFEM 2020, March 1-3, 2021 (postponed), (LNCS 12531) [link]
- Formally Verified Architecture Patterns of Hybrid Systems Using Proof and Refinement with Event-B, In 7th International Conference on Rigorous State Based Methods, ABZ 2020, (postponed but proceedings available), June, 2020, (LNCS 12071) [link]
- Modelling Hybrid Train Speed Controller using Proof and Refinement, In 24th International Conference on Engineering of Complex Computer Systems, ICECCS 2019, Guangzhou, China, November 10-13, 2019, (ISBN 978-1-7281-4647-8) [link]
- Handling Refinement of Continuous Behaviors: A Proof Based Approach with Event-B, In 13th International Symposium on Theoretical Aspects of Software Engineering, July 29-August 1, 2019 [link]
- Hybrid Systems and Event-B: A Formal Approach to Signalised Left-Turn Assist, In 2nd International Workshop on Cybersecurity and Functional Safety in Cyber-Physical System, ICWFS 2018, Marakesh, Morocco, October 24-26, 2018 [link]
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B, In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018 [link]
Journal Papers
- Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems, In ACM Transaction on Embeded Computer Systems (Vol. 20, No. 4), 2021 [link]
Model Driven Engineering for Network Function Virtualisation
Network function virtualisation implements networks as a set of software elements; it can be seen as an extension of machine virtualisation to entire network equipments (routers, links, etc.).
Virtualised networks usually involve numerous different, heterogeneous technologies, that must be precisely and coherently configured in order to obtain a working network.
Since network designers are (generally) not abreast with every technology that exist, and because configuration files are hard to link with the actual network specification, an interesting approach to ease the work of virtual network designers is to propose a high-level domain-specific language, that allows them to express the network in a more adapted and straightforward way.
A sequence of transformations can then be used to derive, from this input specification, a number of configuration files.
In the context of my master, I have developed a tool called MAPLE, able to manage large modelling ecosystems and sequences of transformations, with virtual network design in mind.
This work has been conducted as part of the MAGIC team of the Concordia University (Montréal, Canada), and supervised by Pr. Ferhat Khendek, Dr. Sadaf Mustafiz and Dr. Maria Toeroe.
Publications
Here is a list of publications related to this topic, in descending chronological order.
Conference Papers
- MAPLE: An Integrated Environment for Process Modelling and Enactment for NFV Systems, In ECMFA 2018:14th European Conference on Modelling Foundations and Applications, Toulouse, France, June 26-28, 2018, (LNCS 10890) [link]
- Building domain-specific modelling environments with papyrus: an experience report, In 10th Workshopon Modelling in Software Engineering (MiSE’2018), Gothenberg, Sweden, May 27-28, 2018, (ISBN 978-1-4503-5735-7) [link]
- A Model-Driven Process Enactment Approach for Network Service Design, In SDL 2017:Model-Driven Engineering for Future Internet - 18th International SDL Forum,Budapest, Hungary, October 9-11, 2017, (LNCS 10567) [link]
Journal Papers
- Model-driven process enactment for NFV systems with MAPLE, In Journal of Software System Modelling (SoSyM) (Vol. 19, N. 5), 2020 [link]