Research Interest

My research is focused on advancing formal methods to tackle heterogeneous semantics and create comprehensive approaches for modeling, designing, implementing, and certifying safety-critical cyber-physical systems. To this end, I have identified three primary research areas:

• Modeling, Refinement, and Proofs for State-Based Methods: This involves establishing formal frameworks to ensure the reliability and correctness of state-based systems.

• Software and System Certification: I work on developing standards and methodologies to certify software and systems that are critical to safety and functionality.

• Domain Knowledge Engineering and Invited Semantics: This area aims to enhance modeling and reasoning capabilities through meta-modelling and theoretical frameworks, improving our ability to represent complex systems.

Throughout my research, I have modelled numerous highly critical systems, including cardiac pacemakers, ECG diagnosis medical protocols, adaptive cruise control systems, insulin infusion pumps, landing gear systems, automatic rovers, and ad-hoc network protocols. Additionally, my work also focuses on environmental modelling related to cyber-physical systems. For example, I have developed models of the human heart to verify pacemaker functionality and the glucose homeostasis system to validate insulin infusion pumps.

My major areas of research interest include:

• Logic in Computer Science

• Formal Modeling and Refinement

• Programming Languages

• Formal Methods

• Meta-Modeling

• Domain Knowledge Engineering

• Model Checking

• Environmental or Physical Modeling for Closed-Loop System Verification

• Critical System Development Life-Cycle

• Automatic Code Generation

I also explore applications of software engineering techniques in safety-critical domains. This includes integrating software engineering methodologies with formal methods, conducting hazard analysis, using STPA (Systems-Theoretic Process Analysis), performing requirements analysis, and generating formal models automatically from tabular expressions. I particularly focus on the formal verification of Stateflow models, the certification and re-engineering of the ISO-26262 functional safety standard, and the formal verification of complex medical protocols, distributed systems, concurrent systems, and cyber-physical systems.

Moreover, my interests extend to biomedical signal processing (including ECG and COP signals), artificial neural networks, fuzzy logic, image and video compression, image processing, and blind source separation. This diverse range of research allows me to contribute to the development of robust and dependable systems in critical applications.