Axe(s) de recherche : Systèmes intelligents communiquants
Domaine(s) de compétence :
Embedded systems, Software engineering, Formal methods, Real-time, Automatic control
Ph.D. in Computer Science, Master's degree in Computer Science (field "Software: Formal Methods and Engineering")
BiographieSebti Mouelhi received the undergraduate degree in applied computer science, in 2004, from Ecole Nationale d'Ingénieurs de Carthage, Tunis, Tunisia. He received the M.S. degree in computer science (field "Software: Formal Methods and Engineering"), in 2007, from the University of Lorraine, Nancy, France, and the Ph.D. in computer science, in 2011, from the University of Franche-Comté, Besançon, France. From October 2011 to September 2012, he was hired as postdoctoral researcher at INRIA Grenoble, France. From October 2012 to May 2015, he was R&D engineer at SafeRiver, Montrouge, France. During Summer 2015, he was engineer in safety assurance at ALSTOM Transport, Saint-Ouen, France. He is Assistant Professor at ECE Paris since September 2015.
Retour à la liste des membres
Publications de Sebti MOUELHI
« Predictive Formal Analysis of Resilience in Cyber-Physical Systems »par Sebti MOUELHI
IEEE Access , 7 , pages 33741-33758 , 2019
Liste des auteurs : Sebti Mouelhi, Mohamed-Emine Laarouchi, Daniela Cancila, Hakima Chaouchi
The behavioral analysis of cyber-physical systems in safety-critical scenarios is a challenging task. In this context, the endogenous and exogenous aspects of resilience are of a cornerstone importance in system design and verification. Endogenous resilience is the inherent ability of the system to detect and process internal faults and malicious attacks. Exogenous resilience is the permanent capability of the system to maintain a safe operation within its ambient environment. In this article, we present a predictive dual-sided contract-based formal methodology to address both aspects of resilience on top of a distributed object-oriented component-based software model. It is illustrated by a case study of urban drone rescue systems. We exploit the formalism of timed automata and the toolbox UPPAAL to predict by abstraction and analyze (simulate and verify) endogenous resilience. Instead of presenting the final models of the case study, we reflect our experience with UPPAAL in generic patterns of system design and contract specification, reusable in other contexts with adaptations. The analysis of exogenous resilience is specific to the considered drone rescue system. It consists of synthesizing by iterative model-checking safe flight paths for the drones within a 3D virtual model of urban surroundings true to modern cities.
« Component Design and Adaptation Based on Behavioral Contracts »par Sebti MOUELHI
MEDI'2018 Workshops: New Trends in Model and Data Engineering, CCIS, Springer International Publishing , 929 , pages 217-230 , Marrakech , 2018
Liste des auteurs : Samir Chouali, Sebti Mouelhi, Hassan Mountassir
« Distributed Object-Oriented Design of Autonomous Control Systems for Connected Vehicle Platoons »par Sebti MOUELHI
In proceedings of the 22nd International Conference on Engineering of Complex Computer Systems (ICECCS'17), IEEE , pages 40-49 , Fukuoka, Japan , 2017
Liste des auteurs : Sebti Mouelhi, Daniela Cancila, Amar Ramdane-Cherif
The contribution of this paper is articulated around a new software design approach of autonomous control systems for connected vehicle platoons. Our control system is distributed and real-time based on object-oriented component-based method of design that brakes with the industrial traditions subject to cyclic OS-free approaches. We illustrate our design by relevant case studies of the longitudinal speed control widely studied in industrial and academic research around automotive platooning. Our software is mainly implemented using the Ada standard of programming (in particular the annexes D and E of real-time and distributed systems). The distribution in our software is managed by the versatile middleware PolyORB. The control scenarios and communication aspects covered by the case studies are animated by wheeled robot prototypes commanded by single-board ARM Cortex computers under real-time Linux kernels.
« Safety Controller Synthesis for Incrementally Stable Switched Systems using Multiscale Symbolic Models »par Sebti MOUELHI
IEEE Transactions on Automatic Control , Volume 61, Issue 6 , pages 1537-1549 , 2016
Liste des auteurs : Antoine Girard, Gregor Gössler, Sebti Mouelhi
We propose an approach to the synthesis of safety controllers for a class of switched systems, based on the use of multiscale symbolic models that describe transitions of various durations and whose sets of states are given by a sequence of embedded lattices approximating the state-space, the finer lattices being accessible only by transitions of shorter duration. We prove that these multiscale symbolic models are approximately bisimilar to the original switched system provided it enjoys an incremental stability property attested by the existence of a common Lyapunov function or of multiple Lyapunov functions with a minimal dwell-time. Then, for specifications given by a safety automaton, we present a controller synthesis algorithm that exploits the specificities of multiscale symbolic models. We formalize the notion of maximal lazy safety controller which gives priority to transitions of longer durations; the shorter transitions and thus the finer scales of the symbolic model are effectively explored only when safety cannot be ensured at the coarser level and fast switching is needed. We propose a synthesis algorithm where symbolic models can be computed on the fly, this allows us to keep the number of symbolic states as low as possible. We provide computational evidence that shows drastic improvements of the complexity of controller synthesis using multiscale symbolic models instead of uniform ones.
« Object-Oriented Component-Based Design using Behavioral Contracts: Application to Railway Systems »par Sebti MOUELHI
In Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering (CBSE '15) , pages 49-58 , Montréal, QC, Canada , 2015
Liste des auteurs : Sebti Mouelhi, Khalid Agrou, Samir Chouali, and Hassan Mountassir
We propose a formal approach for the design of object-oriented component-based systems by means of behavioral contracts. This formalism merges interface automata describing communication protocols of components with the semantics of their operations. On grounds of consistency with the object-oriented paradigms, we revisit the notions of incremental design and independent implementability of interface automata by defining otherwise components compatibility, composition, and refinement. The optimistic composition approach of interface automata is adapted to fulfill the interaction aspects of object-oriented components. The composition of two interface automata is computed by removing from their synchronized product all states from which the environment cannot prevent deadlock states (caused by semantic and protocol mismatches) by enabling autonomous (output and local) actions. We define the concept of autonomous actions differently by reclassifying them into method, return, and exception actions. Refinement is intended to ensure an independent implementability of components at the semantic and protocol levels. We present refinement as an expanding simulation relation between interface automata, based on two requirements: (1) a component refinement contains more details about common provided services with the abstraction, and (2) may provide more services than the abstraction. These features lead to define refinement as covariance on input and output events of a component. The alternating simulation originally proposed to refine interface automata, requires contravariance on input and output events, not quite consistent, from our perspective, with the object-oriented context. Our work is illustrated by a design use case of CBTC railway systems to argue their relevance in the safety-critical context.
« CoSyMA: a tool for controller synthesis using multi-scale abstractions »par Sebti MOUELHI
In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC ’13) , pages 83–88 , 2013
Liste des auteurs : Sebti Mouelhi, Antoine Girard, Gregor Gössler
We introduce CoSyMA, a tool for automatic controller synthesis for incrementally stable switched systems based on multi-scale discrete abstractions. The tool accepts a description of a switched system represented by a set of differential equations and the sampling parameters used to define an approximation of the state-space on which discrete abstractions are computed. The tool generates a controller - if it exists - for the system that enforces a given safety or time-bounded reachability specification. We illustrate by examples the synthesized controllers and the significant performance gains during their computation.
« Adaptation sémantique des protocoles des composants par les automates d’interface »par Sebti MOUELHI
Technique et Science Informatiques , Volume 31, Number 6 , 2012
Liste des auteurs : Sebti Mouelhi, Samir chouali, Hassan Mountassir
La réutilisation d’un composant logiciel consiste à l’utiliser dans des contextes différents sans affecter son code et en s’appuyant uniquement sur ses interfaces. En ce sens, il est nécessaire de proposer des techniques d’adaptation des composants permettant d’assurer leur communication malgré les disparités qui peuvent exister au niveau de leurs interfaces. Dans cet article, nous proposons une approche formelle d’adaptation des composants dont les protocoles comportementaux sont décrits par les automates d’interface. Ce formalisme est basé sur une approche optimiste qui considère deux composants comme compatibles s’il existe un environnement convenable avec lequel ils peuvent interagir correctement. L’approche proposée permet, d’une part, d’éliminer les disparités entre deux composants au niveau de la signature, de la sémantique et du protocole, et, d’autre part, de garantir leur compatibilité.
« Refinement of interface automata strengthened by action semantics »par Sebti MOUELHI
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers , Volume 253, Issue 1 , pages 111-126 , 2010
Liste des auteurs : Sebti Mouelhi, Samir chouali, Hassan Mountassir
Interface automata are light-weight models that capture the temporal interface behavior of software components. They have the ability to model both the input requirements and the output behavior of a component. They support the compatibility check between interface models to ensure a correct interaction between components and they adopt an alternating simulation approach to design refinement. In this paper, we extend our previous works on checking interface automata interoperability by adapting their alternating refinement relation to the action semantics. We show the relation between pre and post-conditions of transitions in the abstract version of an interface and their corresponding ones in its concrete version. We illustrate our extensions by a case study of the CyCab car component-based system.
« An I/O automata-based approach to verify component compatibility: application to the CyCab car »par Sebti MOUELHI
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers , Volume 238, Issue 6 , pages 3-13 , 2010
Liste des auteurs : Samir Chouali, Hassan Mountassir, Sebti Mouelhi
An interesting formal approach to specify component interfaces is interface automata based approach, which is proposed by L. Alfaro and T. Henzinger. These formalisms have the ability to model both the input and output requirements of components system. In this paper, we propose a method to enrich interface automata by the semantics of actions in order to verify components interoperability at the levels of signatures, semantics, and protocol interactions of actions. These interfaces consist of a set of required and offered actions specified by Pre and Post conditions. The verification of the compatibility between interface automata reuse the L.Alfaro and T.Henzinger proposed algorithm and adapt it by taking into account the action semantics. Our approach is illustrated by a case study of the vehicle CyCab.