My activities are mainly in the topics:
Internet of Vehicles and urban trafic simulation
Machine learning applied to railway operation & smart urbain mobility
Formal design & verification of real-time, and safety-critical embedded systems : statistical model-checking, formal proofs ...
Component-based applications : synchronous & object-oriented "new" approaches applied to intelligent transportation systems, prototyping ...
Controller synthesis for cyber-physical systems : safety, reachability, learning, tooling ...
Interested in:
Category theory
Cybersecurity: theory, cryptography, exploitation, vulnerabilities, use of formal methods for protocol assessment ...
Wireless communication: theory, protocols, software-defined radio, 5/6G applied to vehicular communication (V2X)
AI & machine learning
Partners:
EGIS Rail
LISV, UVSQ, University of Paris-Saclay
UTAC
5G/6G Innovation Center, University of Surrey ...
Member of the team Systèmes Intelligents Communicants conducted by Laboratoire de Recherche de l'ECE Paris.
Partners:
Laboratoire d'Ingénierie des Systèmes de Versailles (LISV) - UVSQ,
Département d'Informatique des Systèmes Complexes (DISC) - Institut FEMTO-ST,
CEA LIST, CEA Saclay,
Institut VEDECOM ...
PhD Students
Mohamed-Emine Laarouchi (2018-2020) A Safety Approach for CPS-IoT
Co-funded by CEA LIST, SAMOVAR, Telecom SudParis, Institut Polytechnique de Paris
Master and engineering student projects (2018-2020)
Formal design of vehicular communications
Prototyping delay-aware IEEE 802.11p V2X
Formal verification of the CBTC system of Line 13 of Paris subway:
Checking the compliance between the SCADE models of carborne and wayside sub-systems, and their software and system requirements.
Proof language: High Level Language HLL,
Proof assistant: Prover Certifier,
Proof startegies: k-induction, interpolation, and saturation of Stålmarck, ...
Optimization techniques: loop invariants, heuristics, ...
Position: Consultant at Atelier de Qualification Logicielle (AQL) - RATP.
Project: OURAGAN L13.
Partners: THALES Group and Prover Technology.
Design of an SMT-based model-checker for HLL.
Position: Intern at SafeRiver.
Partners: AQL - RATP.
Assessment of the CBTC solution URBALIS Fluence U500:
Failure Mode and Effect Analysis (FMEA) of the software layer,
Formal specification of an internal component-based synchronous language, ...
Position: Intern at ALSTOM Transport.
Project: Modernization of "Métro de Lille Métropole".
FMEA of the solution Tempo CBTC for Singapore's metro lines.
Position: Intern at SafeRiver.
Project: Land Transport Authority (LTA).
Partner: GE Transportation.
Verification and control of cyber-physical and hybrid systems:
Synthesis of safety controllers for switched systems using discrete symbolic models,
Development of the toolbox CoSyMA.
Institution: INRIA Grenoble.
Advised by Antoine Girard and Gregor Goessler.
Project: ANR VEDECY.
Formal verification of object-oriented component-based systems integrity and reuse:
Interoperability (compatibility and substitutability) check of components specified by behavioral contracts, merging their communicating protocols with the semantics of their operations,
Application to Enterprise JavaBeans EJB component model,
Recently (in 2015): re-adaptation and application to railway CBTC signaling systems.
Institution: Institut FEMTO-ST, DISC.
Supervised by Samir Chouali and Hassan Mountassir.
Project: ANR TACOS.
Verification of distributed systems using the pseudo-algorithmic language PlusCAL:
Extension PlusCAL to be compliant with the semantics of distribution,
Modification of the translator to TLA+ (Tamporal Logic of Actions),
Specifying and checking of some basic distributed algorithms.
Institution: LORIA.
Supervised by Stephan Merz and Martin Quinson.