Saddek Bensalem
Professor, Universirsité Grenoble Alpes (UGA)
Contact
Phone: +33 (0)4 38 78 28 06
Fax: +33 (0)4 56 52 03 44
Saddek.Bensalem[at]univ-grenoble-alpes.fr
Laboratoire Verimag
Office location:
Bâtiment IMAG, Université Grenoble Alpes
700 avenue Centrale Domaine Universitaire - 38401 St Martin d'Hères
France
Research interests
I have been leading the "Rigorous System Design" research team, from 2008 to 2020, around the BIP project, with two main directions: 1) the development of verification methods and tools that scale and are usable by engineers ; 2) the design of embedded systems, with an emphasis on the formalization of the design process and the techniques that guarantee correctness by construction. The ambition of the work is to overcome theoretical limitations inherent in the complexity of monolithic verification methods and to conduct a holistic study of the problem of correctness in the general context of a rigorous and mathematically sound design. The BIP framework has found several application domains in practice, with excellent results (robotics, embedded, cyber-physical systems, etc.).
My research activity focuses on rigorous system design as a coherent and accountable process aimed at building cost-effectively systems of guaranteed quality. The aim is to provide the theoretical underpinnings, methods and tools for moving from empirical approaches to a well-founded discipline. Since October 2020, I created a new research project on "Engineering Trustworthy Learning-enabled Systems". The aim of the project is to develop foundations for continuous engineering of trustworthy LE-systems. The targeted scientific breakthrough lies within the convergence of "data-driven" and "model-based" engineering, where this convergence is further complicated by the need to apply verification and validation incrementally and avoid complete re-verification and re-validation efforts. The three scientific directions of this project are: (1) integration of learning-enabled components and model-based components via a contract-based methodology which allows incremental modification of systems including threat models for cyber-security, (2) adaptation of verification techniques applied during model-driven design to learning components in order to enable unbiased decision making, and finally, (3) incremental synthesis techniques unifying both the enforcement of safety properties as well as the optimization of performance.
Thematic mobility
- 1990-03 - Verification of infinite state systems : temporal logics, abstraction parametrized systems, techniques for generation of invariants, deductive methods.
- 2003-07 - Verification methods and testing for real-time and complex systems : Validation of Java real-time programs, synthesis and testing of real-time systems, runtime verification.
- 2007-20 - System design correct by construction : Modelisation and compositional verification of component-based systems, automatic generation of distributed code, design and verification of autonomous systems, generation of invariants, dynamic and reconfigurable architecture, monitoring, statistical model-checking, Mixed-criticality systems.
My research activities, although always related to formal methods and verification a , have evolved during my career, moving from Verification of infinite-state systems, and from testing of real-time systems to design of correct systems by construction".
Geographical mobility
I was a researcher on leave at CNRS from 1998 to 2000 and at CEA from 2012-2014. I spent several months as invited researcher at universities and research institute such as : SRI (sabbatical year in 1996, 3 months in 1997, 8 months in 1998 and 6 months in 1999), Univ. of Kiel (1 month in 1997, 98 and 99), Stanford University (2 months in 1998, 3 months in 2001and 2 months in 2006), Institute Weizmann (2 months in 1999), Univ. of Uppsala (2 months in 2001), Nasa Ames (3 months in 2003), Urbana Champaign Univ. (3 months in 2005), Nasa/JPL (1 month in 2013, 2014 and 2015), Bar Ilan Univ. (1 month in 2013), NIST (4 months in 2016 and 3 months in 2017).
Current Projects
-
FOCETA - H2020 project research and innovation programme under grant agreement No 956123, Oct. 2020 - Oct. 2023.
FOCETA gathers prominent academic groups and leading industrial partners to develop foundations for
continuous engineering of trusworthy learning-enabled autonomous systems. The target scientific breakthrough lies within the convergence of
"data-driven" and "model-based" engineering where this convergence is further complicated by the need to apply verification and validation incrementally
and avoid complete re-verification and re-validation efforts.
-
Brain-IoT - This project receives funding from the European Union’s
Horizon 2020 Framework Programme for Research and Innovation under grant agreement no 780089, Feb. 2018 - March 2021.
BRAIN-IoT aims at establishing a framework and methodology that supports smart autonomous and cooperative behaviors
of populations of heterogeneous IoT platforms that are also closely interacting with Cyber-Physical systems (CPS).
BRAIN-IoT will employ highly dynamic federations of heterogeneous IoT platforms, mechanisms enforcing privacy and
data ownership policies as well as open semantic models enabling interoperable operations and exchange of data and
control features. Brain-IoT will also offer model-based tools easing the development of innovative, tightly integrated IoT and CPS solutions.
-
CPS4EU - CPS4EU is a project funded from the H2020-ECSEL-2018-IA call – Grant Agreement number: 826276, June 2019 - June 2022
CPS4EU proposes to address technical issues and organizational issues in an integrated way. Hence, CPS4EU promotes a high level of sharing, so that an operational ecosystem,
with adequate skills and expertise all along the value chain can enable, at the end of the project, the European industry to lead strategic markets based on CPS technologies.
The ultimate objective of CPS4EU is to strengthen the CPS value chain by creating world class European SMEs and by providing CPS technologies that in turn will sustain
the leadership of the large European groups in key economy sectors and, in this way will stimulate innovative products to support
the massive digitization increasingly integrated into our everyday environment.
Following above statement, ADE proposal is built around the following key aspects: -
ADE - This project has received funding from the European Union’s Horizon 2020 research and
innovation programme under grant agreement No 821988, Feb. 2019 - Feb. 2022.
The overall objective of the Strategic Research Cluster (SRC) in Space Robotics Technologies is to deliver by 2023/2024 key technologies
at a significant scale suitable for two major application domains: orbital and surface exploration. More specifically this 2016 SRC
assumes as reference/target scenarios in-orbit servicing and planetary rover autonomous exploration.
This project, ADE (Autonomous DEcision Making in very long traverses) is targeting the tenth operational Grant (OG10) of the 2018 call. The specific objective of ADE is then to deliver to combine the building blocks from previous PERASPERA projects (OG1 to OG4) in order to test them in a rover planetary application in which all these capabilities will be put in place. In order to achieve this challenging objective, the ADE team has been settled such to guarantee strong background both in robotics in general and operational autonomous space robotic missions, as well as state of the art expertise in each of the previous PERASPERA projects (from Og1-to Og4).
Past Projects
-
ArrowHead - ARTEMIS AIPP, European, 2013-2017
Arrowhead is addressing efficiency and flexibility at the global scale by means of collaborative automation for five application verticals.
That means production (manufacturing, process, energy), smart buildings and infrastructures, electro-mobility and virtual
market of energy.
-
CITADEL - H2020-DS-2015-1 Research and Innovation Framework Programme, 2016-2019.
The project expects to achieve in its final phase the demonstration of the capabilities of the adaptive MILS technology
in several industrial contexts and application scenarios, and lay the technical foundations for a certification
framework for the use of adaptive MILS components and systems in critical infrastructure applications.
-
Transatlantic CPS Summit CT-2014-1c, Coordination & Support Action, European,
2014-2016 Facilitating and promoting EU-US strategic research cooperation in the area of engineering Cyber-Physical Systems.
-
CPSE Labs - H2020-CPS Engineering Labs Innovation Experiment, 2015-2016.
Rigorous framework for developing and validating robotic applications. One objective of this project is to allow verification and
validation of robotic systems at different design levels and thus reach a high degree of maturity at as low as possible cost.
Early discovery of bugs can play a crucial part in reducing design costs for robotic application. Another objective is to provide rigorous
software engineering techniques and tools for correct-‐by-‐construction development of robotic applications.
- ESRoCOS - H2020 project funded by European Commission within Strategic Research Cluster on Space Robotics Technologies. The goal of the ESROCOS project is to provide an open source framework, which can assist in the development of flight software for space robots. By providing an open standard, which can be used by research labs and industry, it is expected thXSat the Technology Readiness Level (TRL) can be made raised more efficiently, and vendor lock-in through proprietary environments can be reduced. Current state-of-the-art robotic frameworks are already addressing some of these key aspects, but mostly fail to deliver the degree of quality expected in the space environment. In the industrial robotics world, manufacturers of robots realise their RCOS by complementing commercial real-time operating systems, with proprietary libraries implementing the extra functions. While this serves the scope of selling robotic systems and applications, it does not provide for a standard for integration of systems and algorithms across multiple vendors. Other open-source frameworks do not have sufficient RAMS properties (e.g. ROS, Orocos, Rock, and Genom) for its use in space missions.
- ERGO - H2020 project funded by European Commission within Strategic Research Cluster on Space Robotics Technologies. The overall objective of the Strategic Research Cluster (SRC) in Space Robotics Technologies is to deliver by 2023/2024 key technologies at a significant scale suitable for two major application domains: orbital and surface exploration. More specifically this 2016 SRC assumes as reference/target scenarios in-orbit servicing and planetary rover autonomous exploration.
- SUCCESS (NEW) CHIST-ERA project-SecUre aCCESSibility for the internet of things. The core idea of SUCCESS is to use methods and tools with a proven track record to provide more transparency of security risks for people in given IoT scenarios. Our core scientific innovation will consist on the extension of well-known industry-strength methods in our priority areas. Our technological innovation will provide adequate tools to address risk assessment and adaptavity within IoT in healthcare environments and an open source repository to foster future reuse, extension and progress in this area. Our project will validate the scientific and technological innovation through pilots, one of which will be in collaboration with a hospital and will allow all stakeholders (e.g. physicians, hospital technicians, patients and relatives) to enjoy a safer system capable to appropriately handle highly sensitive information on vulnerable people while making security and privacy risks understandable and secure solutions accessible.
-
MoSATT-CMP - ESA ITT 1-ITT 1-7646/13/NL/JK, 2014-2016.
Model-based Schedulability Analysis Techniques and Tools for Cached and Multicore Processors.
-
SARGON - ESA AO/1-8355/15/NL/SFe, 2015-2017.
The objectives of SARGON are to:
- produce an assessment of a number of the most-used Open-Source robot controller software (OSRCS) with respect to a number of space application requirements;
- identify the most promising robot controller software (RCS);
- implement and deliver a reference implementation of the RCS.
-
ACOSE - BGLE, Invesstisment d’avenir<, 2011-2014.
-
ACROSS - European IST, FP7, ARTEMIS JU, 2010-2013.
An example for plastic e-service -
ASCENS - European IST, FP7-ICT-2009-5 project number : 257414 , 2010-2014.
-
CERTAINTY - - European IST, FP7, 2011-2013
-
CHAPI - FUI, 2010-2013.
-
COMBEST - FP7 IST STREP 215543, 2008-2010.
-
CyPhERS - European FP7, Support Action, 2013-2015.
-
D-MILS - European STREP FP7, 2012-2015.
-
ManycoreLabs - BGLE, Investissement d’avenir, 2012-2015.
-
MARAE - FNRAE, 2008-2010.
-
MIND Minalogic, 2008-2010.
-
PRO3D - European IST, 2009-2012
-
SMECY - European IST, FP7, ARTEMIS JU, 2010-2013.
Recent publications [all] [dblp] [google scholar]
-
- Souha Ben Rayana, Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Jacques Combaz: Compositional Verification for Timed Systems Based on Automatic Invariant Generation. Logical Methods in Computer Science 11(3) (2015).
- Fotios Gioulekas, Peter Poplavko, Panagiotis Katsaros, Saddek Bensalem, Pedro Palomo: Correction to: Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems. Int. J. Softw. Tools Technol. Transf. 22(1): 33-34 (2020)
- Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, Marius Bozga: A Robust Framework for Securing Composed Web Services. FACS 2015: 105-122
- Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga: Time-Triggered Mixed-Critical Scheduler on Single and Multi-processor Platforms. HPCC/CSS/ICESS 2015: 684-687
- Simon Iosti, Doron Peled, Khen Aharon, Saddek Bensalem, Yoav Goldberg: Synthesizing Control for a System with Black Box Environment, Based on Deep Learning. ISoLA (2) 2020: 457-472
- Mohammed Foughali, Saddek Bensalem, Jacques Combaz, Félix Ingrand: Runtime Verification of Timed Properties in Autonomous Robots. MEMOCODE 2020: 1-12
- Antoine El-Hokayem, Saddek Bensalem, Marius Bozga, Joseph Sifakis: A Layered Implementation of DR-BIP Supporting Run-Time Monitoring and Analysis. SEFM 2020: 284-302
- Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, Marius Bozga: Local Planning Semantics: A Semantics for Distributed Real-Time Systems. Leibniz Trans. Embed. Syst. 6(1): 01:1-01:27 (2019)
- Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga: Priority-based scheduling of mixed-critical jobs. Real Time Syst. 55(4): 709-773 (2019)
- Doron Peled, Simon Iosti, Saddek Bensalem: Control Synthesis Through Deep Learning. From Reactive Systems to Cyber-Physical Systems 2019: 242-255
- Siham Khoussi, Ayoub Nouri, Junxiao Shi, James Filliben, Lotfi Benmohamed, Abdella Battou, Saddek Bensalem: Performance Evaluation of the NDN Data Plane Using Statistical Model Checking. ATVA 2019: 534-550
- Iulia Dragomir, Saddek Bensalem: Rigorous Design of FDIR Systems with BIP. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 77 (2019)