Download ResuméFormal Methods // Formal Modeling // Runtime Verification
Making sure software runs correctly and safely.
Computer and information systems are becoming ubiquitous in everyday life. Human societies now rely heavily on automation. Computer systems are responsible for controlling a wide range of systems forming the infrastructure of a modern society while becoming more complex. As we grow more dependent on them, and as the systems themselves become more complex, it is crucial to be able to know that they are indeed running as expected.
Formal methods are a particular kind of mathematically rigorous techniques for the specification, development and verification of software and hardware systems. Their use is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Dynamic Reconfigurable Systems
The bulk of my work consists in implementing, designing and improving formal modeling techniques for modeling dynamic, reconfigurable, and adaptable systems. These include systems that evolve the number of their components and modify their architecture while executing. Such systems include autonomous systems as well as systems composed of multiple internet of things (IoT) devices.
With Verimag, I am currently working on the Dynamic Reconfigurable BIP (DRBIP) framework to be able to model, simulate, and verify dynamic and reconfigurable systems.
Runtime Verification
Runtime Verification (RV) is a lightweight formal method which consists in verifying that a single run of a system is correct with respect to a formal specification typically expressed in logics (LTL) or finite-state machines.
Most of my work has been in decentralized RV, where there is no central point of observation, but monitors are deployed on different parts of the system to observe separate behavior and communicate so as to have a global view. Decentralized RV has been the bulk of PhD work with Ylies Falcone where we developed the THEMIS framework for designing, simulating, and analyzing decentralized monitoring algorithms.
Featured Papers
When we had no computers, we had no programming problem either.
When we had a few computers, we had a mild programming problem.
Confronted with machines a million times as powerful,
we are faced with a gigantic programming problem.
We present a new two-layered implementation of DR-BIP clearly separating between execution of reconfiguration operations and execution of a fixed system configuration. Such a separation of concerns offers the advantage of re-using the mature and efficient BIP engine. Another direct benefit of the new implementation is the possibility to monitor a holistic view of a system’s behavior captured as a set of traces involving information about both the state of the system components and the dynamically changing architecture.
We present a data structure that (i) keeps track of the execution of an automaton (ii) has predictable parameters and size and (iii) guarantees strong eventual consistency. We introduce decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study two properties of decentralized specifications pertaining to monitorability and compatibility between specification and architecture. We also present a general algorithm for monitoring decentralized specifications. Furthermore, we present THEMIS, a framework for designing such decentralized algorithms and simulating their behavior.
In this tutorial, we review some of the main RV approaches and tools that handle multithreaded Java programs. We discuss their assumptions, limitations, expressiveness, and suitability when tackling parallel programs such as producer-consumer and readers-writers. By analyzing the interplay between specification formalisms and concurrent executions of programs, we identify four questions RV practitioners may ask themselves to classify and determine the situations in which it is sound to use the existing tools and approaches.
We use runtime verification (RV) to check various specifications in a smart apartment. The specifications can be broken down into three types: behavioral correctness of the apartment sensors, detection of specific user activities (known as activities of daily living), and composition of specifications of the previous types.
The context of the smart apartment provides us with a complex system with a large number of components with two different hierarchies to group specifications and sensors: geographically within the same room, floor or globally in the apartment, and logically following the different types of specifications.
Get to know me
About Me
I like tackling problems that impact people in real situations, and try to resolve those with the help of the involved people and my specialized skill-set to tailor an appropriate approach.
I do not shy away from a challenging problems and enjoy taking on difficult tasks, and I am very open to learning as I go along the way.
-
Balance
01.Balance the Theoretical and the Practical
I like a healthy balance of theoretical and practical problems. I enjoy most when my solution have direct impact on people and the real world.
I appreciate rigour and elegance.
-
Reproducible Research
02.Reproducibility of Academic Research
I try to always provide an artifact of data and documentation to reproduce or at least replicate my research.
At the very least, I believe public research should be accessible to everyone.
-
Autonomy
03.Freedom to experiment and take decisions
As a tinkerer, I appreciate being given the time to manage my own time and processes while being allowed to experiment with ideas.
This also extends for IP outside works.
Postdoctoral Researcher
The bulk of my research work consists in implementing, designing and improving formal modeling and verification techniques for modeling dynamic, reconfigurable, and adaptable systems. I am working primarily on extending the DR-BIP framework to handle verification of complex autonomous systems scenarios.
My research work in Verimag is in the context of the EU project CPS4EU, I work to provide the necessary adaptation, and extensions of our tools to support our partners in the project.
I am also exploring formal approaches to apply more rigour to the guarantees on the output of Neural Networks (with ReLU layers).
Université Grenoble Alpes
Grenoble, France 2015 - 2018PhD Computer Science
My PhD was done in the Laboratoire d'Informatique de Grenoble with the CORSE team, under the supervision of Yliès Falcone. My thesis is titled: "Runtime Verification of Hierarchical Decentralized Specifications".
The main motivation was to provide multiple specifications to different parts of a systems. This would allow diffent monitors to be deployed for each specification, and communicate to achieve a global verification of the system. Specifications usually express some dependencies on others, and part of the work was also to define properties on decentralized specifications.
With decentralized specifications, we can mix and match specifications that may not necessarily be rigorous, so long as they return a Boolean verdict. This allows specifications to be constructed using some hybrid parts with machine learning or other systems without knowing their internals.
During my PhD, I also developed the THEMIS framework to provide all the support to study decentralized monitoring.
I also was a TA for Automata and Languages for two fall semesters.
American University of Beirut
Beirut, Lebanon 2013 - 2015M.Sc Computer Science (4.0 GPA)
- Thesis: A General Framework for the Integration of Crosscutting Concerns in BIP
- Advisor: Mohamad Jaber
Additionally did some research on parallel software with Fatima Abu Salem and helped documenting some features of the university's high performance cluster.
Awarded Computer Science Student of the Year (2015), which is awarded to the student who demonstrated remarkable services to the department, and excellent research and academic record.
- Courses I assisted with: Parallel Programming, Operating Systems, Programming (with Java), and General Computer Literacy.
Cashunited Moneygram
Badaro, Lebanon 2010 - 2012Developer and IT
- Designed and Implemented a CRM web application that interfaces with the internal call center (Asterisk and IP PBX) and the various company systems (.NET apps, web services) to improve customer support.
- Before automating the processes for the application, I helped with the various department leads and management to streamline the customer support processes and improve their quality.
- Helped implement systems (and web services) for money transfer between our local services and foreign banks.
- Assisted staff with IT support with our internal systems.
- Developed various small tools to help staff perform their daily operations: scripts to streamline data processing, GIS tools to help with locating shops to redirect customers.
Freelancer
2006 - 2015Full-Stack Web Developer
- Worked on multiple paid projects: social media, content creation platforms, web design, web services and applications.
- I also work on personal projects for small communities, particularly around social work and video games.
Notre Dame University
Zouk Mosbeh, Lebanon 2008 - 2012B.Sc Computer Science (3.7 GPA)
Graduation project handled the implementation of aspect oriented techniques for PHP.
Non-exhaustive list of
Things I worked with
Ant, Antlr, Java, C/C++, Matlab, Scheme, Bash, AspectJ, ASM, Git, R, Docker, Behavior Interaction Priority (BIP), Eclipse, IntelliJ, EMF Modeling, Acceleo, Z3 (SMT-LIB), Unity
Languages
Hobbies
I find plenty of activities absolutely fascinating.
For an exquisite video, click on the top right icon.
