VLDB 2026 Research / reviewers in the wild / expert
Olfa Mosbahi
dblp:36/5679
· DBLP profile ↗
47ranked-venue papers
5as first author
7since 2021 · last 2025
0000-0002-0971-2368ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 17 · 2 first-author · 4 since 2021Human-computer interaction and ubiquitous computing · 9 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 9 · 1 first-author · 1 since 2021Artificial intelligence and machine learning · 8 · 3 since 2021Systems, architecture and hardware · 6 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Investigating the performance of multi-objective reinforcement learning techniques in the context of IoT with harvesting energy
Bakhta Haouari, Rania Mzid, Olfa Mosbahi |
J. Supercomput. | 3 |
| 2024 | Reinforcement Learning for Multi-Objective Task Placement on Heterogeneous Architectures with Real-Time Constraints
Bakhta Haouari, Rania Mzid, Olfa Mosbahi |
ENASE | 3 |
| 2024 | Analyzing MQTT Attack Scenarios: A Systematic Formalization and TLC Model Checker Simulation
Amina Jandoubi, Mohamed Taha Bennani, Olfa Mosbahi, Abdelaziz El Fazziki |
ENASE | 3 |
| 2024 | Multi-Criteria Decision-Making Approach for an Efficient Postproduction Test of Reconfigurable Hardware System
Asma Ben Ahmed, Fadwa Oukhay, Olfa Mosbahi |
ICSOFT | 3 |
| 2023 | PSRL: A New Method for Real-Time Task Placement and Scheduling Using Reinforcement LearningabstractModern real-time system development methodologies describe a stage in which application tasks are deployed onto an execution platform.The deployment process is divided into two steps: (i) task placement on processors and (ii) task scheduling to determine their execution order.The overall performance of the deployment model depends on the two steps, which are interdependent.In this paper, a new method based on reinforcement learning techniques, called PSRL, is proposed.PSRL explores all the feasible placements in the first step.In the second step, an optimal schedule is considered for each feasible placement.PSRL generates the optimal deployment, which corresponds to the placement and scheduling that minimize task response times.Application to case studies shows the applicability and quality of the obtained solutions when compared to related work. Bakhta Haouari, Rania Mzid, Olfa Mosbahi |
SEKE | 3 |
| 2023 | A reinforcement learning-based approach for online optimal control of self-adaptive real-time systems
Bakhta Haouari, Rania Mzid, Olfa Mosbahi |
Neural Comput. Appl. | 3 |
| 2022 | On the Use of Reinforcement Learning for Real-Time System Design and Refactoring
Bakhta Haouari, Rania Mzid, Olfa Mosbahi |
ISDA (3) | 3 |
| 2020 | Performance Optimization of Reconfigurable Real-Time Wireless Sensor NetworksabstractWireless sensor networks (WSNs) can be seriously impacted by several changes in behavior. As a measure of optimality, a network should react in real-time. However, even if some reactions can make the system flexible, they can cause significant damages when they are not well-structured. Moreover, the scenarios of reconfigurations can affect several parameters within a wireless sensor network. Among these parameters it is possible to name the energy efficiency, the memory limitation within a node, the real-time constraints at the level of the nodes and the network in general. Either through the application or the transmission of the reconfiguration scenarios, some parameters are severely altered. A metamorphosis of the internal architecture of the nodes is proposed in this research work as well as a policy of communication between several nodes aiming to adapt the network to any change. The resulting proposition offers general efficiency in energy and real-time constraints. The efficiency is realized by the application of a pipelined approach, dealing with the incoming reconfiguration scenarios, and a communication protocol, based on a priority energy and deadline aware scheduling algorithm (a multicriteria scheduling algorithm). This protocol is capable of optimizing the transmission of both reconfiguration scenarios and sensed data simultaneously. The solution is tested on a network connecting several cars during an automobile journey and the results validate the efficiency of this proposition. Maroua Gasmi, Olfa Mosbahi, Mohamed Khalgui, Luís Gomes 0001, Zhiwu Li 0001 |
IEEE Trans. Syst. Man Cybern. Syst. | 2 |
| 2020 | An Extended Object Constraint Language for Adaptive Discrete Event Systems With Application to Reconfigurable Wireless Sensor NetworksabstractThis paper deals with software validation of flexible discrete-event systems. A reconfiguration scenario is any run-time adaptation of the software execution according to user requirements. Nevertheless, since several behaviors can be redundant from an execution to another, using the object constraint language (OCL) is not useful to specify all constraints that should be satisfied by a system. We propose an extension of OCL named reconfigurable OCL for improving the specification and validation of constraints related to different execution scenarios of a system. An ROCL metamodel is proposed with formal syntax and semantics. This solution gains in terms of validation time and quick expressions of constraints. We apply the proposed extended language to reconfigurable wireless sensor networks to highlight the benefits of this contribution. Hanen Grichi, Olfa Mosbahi, Mohamed Khalgui, Zhiwu Li 0001 |
IEEE Trans. Syst. Man Cybern. Syst. | 2 |
| 2019 | Cooperative Energy Management Software for Networked Microgrids
Ilyes Naidji, Olfa Mosbahi, Mohamed Khalgui, Abdelmalik Bachir |
ICSOFT | 2 |
| 2018 | Enhanced Test for Reconfigurable Hardware Systems Based on Sequential LogicabstractThis paper revolves around a test of a reconfigurable hardware system based on sequential logic (abbreviated, RHSS). The latter is a sequential hardware device that allows to change the hardware resources at run-time in order to modify the system functions and therefore to dynamically adapt the system to its environment. In order to reduce time and effort for finding test patterns and analyzing a circuit for its faults, we endeavor to show the way inter-circuits fault collapsing for RHS based on combinational logic remains valid and can be extended to RHSS. The application of the inter-circuits technique reduces the number of faults dealt with by eliminating redundant faults existing between circuits composing the RHSS. For a scalable RHSS, it is often impractical to reach an overall fault coverage. We propose two test techniques that target a minimal necessary set of faults while ensuring an acceptable fault coverage that answers the manufacturer requirements. For so doing, we promote a guiding method for rating potential faults in terms of their occurrence and severity where a fault is weighted according to how serious its consequence and how frequent it can occur. The proposed approach is implemented in a new version of the original TnTest tool. Asma Ben Ahmed, Olfa Mosbahi, Mohamed Khalgui |
EUC | 2 |
| 2018 | Toward a New Methodology for an Efficient Test of Reconfigurable Hardware SystemsabstractThis paper deals with the test of a reconfigurable hardware system (RHS). The latter is a hardware device that allows to change the hardware resources at runtime in order to modify the system functions and therefore to dynamically adapt the system to its environment. The increasing functional complexity of embedded systems and the transition to the RHS make the hardware testing a challenging task, especially under the confine of providing a high quality with a low cost. Considering the fact that the hardware test represents a key cost factor in a production process, an optimal test strategy can be advantageous in the competitive industrial market. Accordingly, this paper introduces a new methodology for an efficient hardware test of RHS. For an RHS, the number of stuck-at faults can be very large, which leads to a significant slowdown in the testing process. Because of the redundancy of faults between the different circuits composing an RHS, the proposed methodology aims at minimizing the number of faults using the inter-circuits relationships and consequently at providing an optimal fault set that can be effectively used for testing. Efficient techniques for test generation and test set validation are proposed to provide the test patterns for faults reduced by inter-circuits fault collapsing. The application of the generated test patterns is typically sufficient to provide an overall fault coverage. The proposed methodology is implemented in a new visual environment named TnTest. An experimental study confirms and validates the expected findings. Note to Practitioners-This paper addresses possible challenges for future generations of adaptive embedded systems. It proposes an original methodology for an efficient reconfigurable hardware system (RHS) hardware test. The main objective is to significantly reduce time and cost needed for the testing process. For an RHS, the number of stuck-at faults can be very large, which can cause a major slowdown in the hardware test. Based on the inter-circuits relations existing between the different circuits composing an RHS, the proposed methodology decreases considerably not only the number of the faults but also the test patterns needed for testing. The application of the generated test patterns is typically sufficient to provide an overall fault coverage. The proposed methodology is implemented in a new visual software environment named TnTest, which is capable of providing the smallest fault set as well as the efficient test set that can be effectively used for testing. This environment can be applied to test any embedded device that can be deployed in any new application based on flexible technologies. It can also be useful in manufacturing industries for a required improvement of the production process in relation to time and cost. Asma Ben Ahmed, Olfa Mosbahi, Mohamed Khalgui, Zhiwu Li 0001 |
IEEE Trans Autom. Sci. Eng. | 2 |
| 2018 | R-Node: New Pipelined Approach for an Effective Reconfigurable Wireless Sensor NodeabstractThe pipeline of reconfiguration is a novel approach that gives a decision making mechanism for any system of tasks when several reconfiguration scenarios are required. These scenarios represent the run-time operations that allow automatic functional modification of the system behavior. In the case of their frequent income, the pipeline follows a specific set of steps in order to figure out the scenarios that need to be applied without altering its own performance. The steps are represented by a sequence of modules. The first module checks the availability of the resources needed by the tasks. The second maintains the stability by rejecting any insupportable flow of software reconfigurations that can destabilize a system. The third module checks the availability of memory for each software reconfiguration request, whereas the fourth verifies the availability of energy for the execution of a new system software configuration. The last module checks the schedulability of this configuration by changing the priorities of the finally accepted tasks in order to reduce their response and blocking times, and to meet their deadlines. The feasibility of the reconfiguration through this approach allows its implementation in wireless sensor nodes. Known by their important requirements in terms of memory and energy, this proposition is adequate when it comes to guaranteeing a maximum lifespan of the nodes. Therefore, the pipeline of reconfiguration is integrated as a middleware within the software architecture of a node. The functionality of this middleware is coordinated by the mean of a set of threads that manage the communication between the pipeline of reconfiguration and the operating system. A tool has been developed within LISI Laboratory to encode this proposition and show its impact on a large range of real devices under diversified scenarios of reconfigurations. Maroua Gasmi, Olfa Mosbahi, Mohamed Khalgui, Luís Gomes 0001, Zhiwu Li 0001 |
IEEE Trans. Syst. Man Cybern. Syst. | 2 |
| 2018 | New Power-Oriented Methodology for Dynamic Resizing and Mobility of Reconfigurable Wireless Sensor NetworksabstractThis paper deals with reconfigurable wireless sensor networks (RWSNs) that should be adapted to their environment in order to minimize the energy consumption during the communication among nodes and consequently to maximize the lifetime of the network as much as possible. An RWSN is assumed to be composed of a set of nodes located in distributed zones such that each node executes reconfigurable software tasks to control local sensors. We propose in a previous work a zone-based multiagent architecture for an RWSN where a communication protocol is well-defined to optimize distributed reconfigurations. This architecture combines all possible reconfiguration forms of the network to be adapted to its environment under energy constraints. With the multiagent architecture we gain in term of energy to be consumed by each node in the network. After applying a set of reconfiguration scenarios, the total charge of the network decreases. In order to preserve this charge as much as possible before the next recharging operation, in this particular study, we tend to resize geographically the zones in an RWSN. We propose also to move the mobile nodes in order to increase the network lifetime. A new run-time power oriented methodology is reported, which manages the zones and their mobile nodes in order to control the energy consumption. Two dynamic solutions are applied: 1) the resizing of zones and 2) the mobility of nodes. For the new proposed methodology, we present a set of equation systems to model the resizing of zones and the mobility of nodes. The solution of these systems allows us to conclude that we can conserve more energy during the communication among network elements (nodes, stations, and agents). The contributions are applied to a case study that we simulate with the reconfigurable wireless network environment1to analyze the research originality. Hanen Grichi, Olfa Mosbahi, Mohamed Khalgui, Zhiwu Li 0001 |
IEEE Trans. Syst. Man Cybern. Syst. | 2 |
| 2017 | Adaptive Task Mapping and Scheduling for Reconfigurable Distributed Embedded Energy Harvesting SystemsabstractAs with the requirements of high-performance and flexible computing, reconfigurable computing systems have become a subject of a great deal of research. Reconfigurable computing systems have to deal with unpredictable events from the environment such as arrival of new tasks, and hardware or software failures, by adapting the task allocation and scheduling, in order to maintain the system feasibility and performance. This paper presents a novel adaptive approach to address the real-time task scheduling issue in reconfigurable multiprocessor embedded systems based on energy harvesting with the consideration of system performance optimization. An energy efficient offline task mapping and scheduling algorithm is proposed to balance the workload in the multiprocessor embedded system. In order to optimize the system performance and to guarantee the system correctness in the presence of reconfiguration scenarios, a distributed control system is built to process a task migration. A cost function to evaluate the energy and time overheads of tasks migration is proposed. Extensive performance evaluations show the effectiveness of the proposed approach in terms of deadline miss ratio, and the energy gain compared with the related state-of-the-art techniques. Wiem Housseyni, Olfa Mosbahi, Mohamed Khalgui |
AICCSA | 2 |
| 2017 | REHLib: New Optimal Implementation of Reconfigurable Energy Harvesting Multiprocessor Systems
Wiem Housseyni, Olfa Mosbahi, Mohamed Khalgui |
ICSOFT | 2 |
| 2017 | New Verification Approach for Reconfigurable Distributed Systems
Oussama Khlifi, Olfa Mosbahi, Mohamed Khalgui, Georg Frey |
ICSOFT | 2 |
| 2017 | Specification Approach using GR-TNCES: Application to an Automotive Transport System
Oussama Khlifi, Christian Siegwart, Olfa Mosbahi, Mohamed Khalgui, Georg Frey |
ICSOFT | 3 |
| 2017 | RWiN: New Methodology for the Development of Reconfigurable WSNabstractThis paper presents new challenges for the development of reconfigurable wireless sensor networks (RWSNs) that adapt dynamically their behaviors to their environment under different properties. An RWSN is a set of networked nodes that execute reconfigurable software tasks for the control of local sensors. We propose a new design methodology named RWiN of an RWSN using unified modeling language (UML) to analyze, construct, develop, and verify easily RWSN architectures. For that, we formulate a metamodel of RWSN based on UML to describe a zone-based architecture that uses a communication protocol for the optimization of distributed reconfigurations. To control the design complexity, we model each agent of this architecture by nested state machines. To verify the temporal constraints by communicating agents, each one is modeled by a timed automaton. The paper's contribution is applied to a case study, which is simulated with TRMSim-WSN and UPPAAL environment to expose the originality of this new architecture. Hanen Grichi, Olfa Mosbahi, Mohamed Khalgui, Zhiwu Li 0001 |
IEEE Trans Autom. Sci. Eng. | 2 |
| 2016 | Real-time scheduling of sporadic tasks in energy harvesting distributed reconfigurable embedded systemsabstractThis paper explores the energy-aware strategy for adaptive task allocation of sporadic task model in distributed reconfigurable embedded systems powered by a renewable energy source. It is challenging to ensure hard real-time deadlines of sporadic tasks in distributed reconfigurable embedded systems that entirely rely on energy harvesting with limited capacity storage because their release times and periods are unknown beforehand. In this regard, we propose a new scheduling algorithm for sporadic task model in energy harvesting reconfigurable distributed embedded system. The proposed approach generates an energy efficient offline task assignment heuristic. Then, the offline stage is dynamically extended online by applying a dynamic adaption algorithm. The latter performs three solutions: (i) Migration, (ii) Degradation of the execution mode, and (iii) Removal of tasks in order to maintain schedulability and sustainability of the application software. Simulations show the efficiency of the proposed approach in term of deadline success ratio. Wiem Housseyni, Olfa Mosbahi, Mohamed Khalgui, Maryline Chetto |
AICCSA | 2 |
| 2016 | Real-Time Scheduling of Reconfigurable Distributed Embedded Systems with Energy Harvesting PredictionabstractIn this paper, we are interested in real-time scheduling of a distributed reconfigurable embedded system powered by a renewable energy source. Uncertainty of energy availability in energy harvesting systems makes the problem of task scheduling more challenging. A reconfiguration scenario is defined as an operation that allows the addition-removalmodification of tasks which may result in timing infeasibility. The system updates its behaviour in accordance with user requirements in reaction to unpredictable events from the environment. The contribution of this paper concerns energyaware strategies for adaptive task allocation. The proposed approach is decomposed into two phases a) Static task assignment heuristic, and b) Dynamic adjustment algorithm. In order to maintain schedulability and sustainability of the application software, the dynamic adjustment algorithm performs three functions: i) Migration, ii) Degradation of the execution mode, and iii) Removal of tasks. We employ a novel energy prediction algorithm. A simulation study brings to light the effectiveness of the proposed approach in terms of deadline success ratio. Wiem Housseyni, Olfa Mosbahi, Mohamed Khalgui, Maryline Chetto |
DS-RT | 2 |
| 2016 | RA2DL-Pool: New Useful Solution to Handle Security of Reconfigurable Embedded SystemsabstractInternational audience Farid Adaili, Olfa Mosbahi, Mohamed Khalgui, Samia Bouzefrane 0001 |
ENASE | 2 |
| 2016 | A Novel R-UML-B Approach for Modeling and Code Generation of Reconfigurable Control SystemsabstractThis research paper deals with the modeling and code generation of Reconfigurable Control Systems (RCS) following UML and B methods. Reconfiguration means dynamic changes of the system behavior at run-time according to well-defined conditions to adapt it to its environment. A reconfiguration scenario is applied as a response to user requirements or any possible evolution in its environment. We affect a Reconfiguration Agent (RA) to RCS to apply an automatic reconfiguration. A new approach called (R-UML-B) is proposed. It consists of three complementary phases: UML specification, B specification and the simulation phase. The first phase models the RCS following UML class and state diagrams. The second phase translates UML specification into B specification according to the well-defined rules and R-UML-B formalism to define the Behavior, Control, Listener, Database and Executive modules of the RCS. Then, we determine the refinement model and the code generation of the B abstract model in C code. We verify the RCS by following the B method in order to guarantee the consistency and the correctness of the specification, refinement and code generation levels. The third phase imports the generated C code to implement a simulator, named B Simulator in order to test and validate the proposed approach. All the contributions of this work are applied to the benchmark production system EnAS. Raja Oueslati, Olfa Mosbahi, Mohamed Khalgui, Samir Ben Ahmed |
ENASE | 2 |
| 2016 | Modeling and Simulation of an Energy Efficient Skid Conveyor using ZIZOabstractThis paper introduces a method for modeling and simulation of a production system with different energy modes. We aim to save the energy in an assembly automobile production line platform using sensitive sensors. A new prototype model is proposed using an extension of Petri nets called GR-TNCES (generalized reconfigurable timed net condition event systems). We also present a simulation of this model with a proposed tool ZIZO to show the energy gain compared to standard production line model. Oussama Khlifi, Christian Siegwart, Olfa Mosbahi, Mohamed Khalgui, Georg Frey |
ICINCO (1) | 3 |
| 2016 | A Development Tool Chain for Reconfigurable WSNsabstractThis paper deals with reconfigurable wireless sensor networks (RWSN) in which a reconfiguration scenario is assumed to be any run-time adaptation of the software execution according to user requirements. We present a Reconfigurable Wireless Network Environment (RWiN-Environment) which is a visual tool allowing for designers to develop RWSN by starting from the initial specification and modeling of the architecture, then the required formal verification based on UPPAAL to verify temporal and functional properties described in user requirements. RWiN-Environment allows also the software design as well as the constraints validation by using an extension of OCL for optimization. The last step in the development process deals with the code generation and also the final deployment on STM32F4-based WSN. The developed tool is applied to a simulated case study in order to control an irrigation system in the agriculture domain. Hanen Grichi, Olfa Mosbahi, Mohamed Khalgui |
SoMeT | 2 |
| 2015 | New Solutions for Useful Execution Models of Communicating Adaptive RA2DL
Farid Adaili, Olfa Mosbahi, Mohamed Khalgui, Samia Bouzefrane 0001 |
SoMeT | 2 |
| 2015 | PEDASA: Priority, Energy and Deadline Aware Scheduling Algorithm
Maroua Gasmi, Olfa Mosbahi, Mohamed Khalgui, Luís Gomes 0001 |
SoMeT | 2 |
| 2015 | Dynamic Low-Power Reconfiguration of Real-Time Systems With Periodic and Probabilistic TasksabstractThis paper deals with the dynamic low-power reconfiguration of a real-time system. It processes periodic and probabilistic tasks that have hard/soft deadlines corresponding to internal/external events. A runtime event-based reconfiguration scenario is a dynamic operation allowing the addition/removal of the assumed periodic/probabilistic tasks. Thereafter, some tasks may miss their hard deadlines and the power consumption may increase. In order to reconfigure the system to be feasible, i.e., satisfying its real-time constraints with low-power consumption, this research presents a software-agent-based architecture. An intelligent agent is developed, which provides four solutions to reconfigure the system at runtime. For these solutions, in order to reconfigure the probabilistic tasks to be feasible, the agent modifies their temporal parameters dynamically; moreover, in order to feasibly serve the probabilistic tasks and reduce the system's power consumption, the agent provides three virtual processors by dynamically extending the periods of the periodic tasks. A simulation study verifies the effectiveness of the agent. Xi Wang 0015, Imen Khemaissia, Mohamed Khalgui, Zhiwu Li 0001, Olfa Mosbahi, MengChu Zhou |
IEEE Trans Autom. Sci. Eng. | 5 |
| 2015 | Corrections to "Deadlock Prevention for a Class of Petri Nets With Uncontrollable and Unobservable Transitions"abstractIn the above paper [8, p. 733], there are errors inTheorem 1: Zhiwu Li 0001, MengChu Zhou, Mohamed Khalgui, Olfa Mosbahi |
IEEE Trans. Syst. Man Cybern. Syst. | 5 |
| 2014 | Reconfigurable Priority Ceiling Protocol - Under Rate Monotonic Based Real-time SchedulingabstractThis research paper deals with reconfigurable real-time systems to be adapted to their environment under user requirements. A reconfiguration scenario is a run-time software operation that allows the addition, removal and update of real-time OS tasks which can share resources and should meet corresponding deadlines. We propose a new Reconfigurable Priority Ceiling Protocol (denoted by RPCP) that avoids deadlocks after any reconfiguration scenario and changes the priorities of tasks in order to reduce their response and blocking times, and to meet their deadlines. This protocol requires the use of two virtual processors in order to guarantee the non-interruption of execution during the reconfiguration step. We develop a tool that encodes this protocol which is applied to a case study. Maroua Gasmi, Olfa Mosbahi, Mohamed Khalgui, Luís Gomes 0001 |
ICINCO (1) | 2 |
| 2014 | Reconfigurable CAN in Real-time Embedded PlatformsabstractThis paper1 deals with the dynamic reconfiguration of the frame packing as well as the traffic of real-time packets on a CAN network. This network is assumed to link distributed reconfigurable STM32F4 microcontrollers that can automatically add-remove-update periodic and aperiodic OS tasks at run-time. These tasks may exchange messages to be loaded in packets and to be sent on the network. After the addition of a pair of dependent tasks on two microcontrollers, a message should be added on CAN and should respect a corresponding deadline related to these tasks. After several additions of messages, some deadlines may be violated and the CAN may not support the added messages. In addition, the frame packing should be adapted at run-time to any reconfiguration scenario in the different microcontrollers. We propose a multi-agent based architecture to check the correct transmission of messages. If some deadlines are violated, these agents propose technical solutions for the feasibility of the whole system. They can suggest first the modification of periods or deadlines of tasks and messages. They can propose also the removal of some OS tasks or messages from the controllers according to their priorities. We propose in addition new solutions to construct the dynamic frame-packing while the bandwidth is minimized. A tool is developed at LISI and Cynapsys to support the different contributions of this paper. Imen Khemaissia, Olfa Mosbahi, Mohamed Khalgui |
ICINCO (1) | 2 |
| 2014 | New Solutions for Modeling and Verification of B-based Reconfigurable Control SystemsabstractThe paper deals with the modeling and verification of B method-based reconfigurable control systems. Reconfiguration means the dynamic changes of the system behavior at run-time according to well-defined conditions to adapt it to its environment. A reconfiguration scenario is applied as a response to improve the system's performance, or also to recover and prevent hardware/software errors, or also to adapt its behavior to new requirements according to the environment evolution. A new extension called Reconfigurable B “R-B” is proposed to specify reconfigurable control systems. It consists of two modules: Behavior and Control. The first defines all possible behaviors of the system, and whereas the second is a set of reconfiguration functions applied to change the system from a behavioral configuration to another one at run-time. We verify a reconfigurable control system by using the B method. The goal is to guarantee the consistency and the correctness of the abstract specification level. The second contribution of this paper deals with the verification of the reconfigurable system by avoiding redundant checking of different behaviors sharing similar operations. In order to control the complexity of verification, an optimal algorithm is developed and a prototyped tool called “Check R-B” is implemented. The paper's contribution is applied to a benchmark production system FESTO. Raja Oueslati, Olfa Mosbahi, Mohamed Khalgui, Samir Ben Ahmed |
ICINCO (1) | 2 |
| 2013 | Runtime Reconfigurations of Embedded ControllersabstractNo abstract available. Mohamed Khalgui, Olfa Mosbahi, Zhiwu Li 0001 |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2013 | Combining Formal Methods for the Development of Reactive SystemsabstractThis article deals with the use of two verification approaches: theorem proving and model checking. We focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA + by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA + to verify liveness properties on a software behavior. We extend first the expressivity and the semantics of a B model (called temporal B model ) to deal with the specification of fairness and eventuality properties. Second, we give transformation rules from a temporal B model into a TLA + module. We present in particular, our prototype system called B2TLA + , that we have developed to support this transformation; then we can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams. We illustrate our approach on a case study of a parcel sorting system. Olfa Mosbahi |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2013 | R-TNCES: A Novel Formalism for Reconfigurable Discrete Event Control SystemsabstractThis study deals with the formal modeling and verification of reconfigurable discrete event control systems (RDECSs). The behavior of an RDECS is represented by that of control components (CCs) and the communication among them. A new formalism, called Reconfigurable Timed Net Condition/Event Systems (TNCES) (R-TNCES), is proposed for the optimal functional and temporal specification of RDECS, which is defined by a behavior module and a control module. The former is a union of various superposed TNCESs, where TNCES-based CC modules are basic units. The latter is a set of reconfiguration functions dealing with the automatic transformations of these TNCESs in response to errors or user requirements by enabling or disabling CC modules, changing condition signals and/or event signals among them, and also treating the state feasibility before and after reconfigurations. To control the verification complexity of R-TNCES, a layer-by-layer verification method is developed, where the similarities of different TNCESs in the behavior module are considered. The contribution of this original paper is applied to a benchmark production system. Mohamed Khalgui, Zhiwu Li 0001, Olfa Mosbahi, Abdulrahman Al-Ahmari |
IEEE Trans. Syst. Man Cybern. Syst. | 4 |
| 2012 | Corrections to "Design of a Maximally Permissive Liveness-Enforcing Petri Net Supervisor for Flexible Manufacturing Systems"abstractPresents corrections to the second paragraph of Section V-B in the above titled paper (ibid., vol. 8, no. 2, pp. 374-393, Apr. 2011). Yufeng Chen 0001, Zhiwu Li 0001, Mohamed Khalgui, Olfa Mosbahi |
IEEE Trans Autom. Sci. Eng. | 4 |
| 2012 | Deadlock Prevention for a Class of Petri Nets With Uncontrollable and Unobservable TransitionsabstractThis study deals with deadlock problems in a system with uncontrollable and unobservable events, which is modeled with a subclass of Petri nets. We design monitors to enforce constraints for minimal siphons in a Petri net model. A key point of this paper is how to select the input and output arcs of a monitor when there exist uncontrollable and unobservable transitions. After the enforcement of constraints, an iterative algorithm is developed to obtain a controlled system with liveness. A sufficient and necessary condition is established to decide the existence of a monitor enforcing a constraint in a plant with uncontrollable and unobservable transitions. Zhiwu Li 0001, MengChu Zhou, Mohamed Khalgui, Olfa Mosbahi |
IEEE Trans. Syst. Man Cybern. Part A | 5 |
| 2011 | Feasible Dynamic Reconfigurations of Petri Nets - Application to a Production System
Mohamed Khalgui, Olfa Mosbahi, Zhiwu Li 0001, Atef Gharbi |
ICSOFT (2) | 2 |
| 2011 | A formal approach for the development of reactive systems
Olfa Mosbahi, Leila Ben Ayed, Mohamed Khalgui |
Inf. Softw. Technol. | 1 |
| 2011 | Design of a Maximally Permissive Liveness- Enforcing Petri Net Supervisor for Flexible Manufacturing SystemsabstractDeadlock prevention plays an important role in the modeling and control of flexible manufacturing systems (FMS). This paper presents a novel and computationally efficient method to design optimal control places, and an iteration approach that only computes the reachability graph of a plant Petri net model once in order to obtain a maximally permissive liveness-enforcing supervisor for an FMS. By using a vector covering approach, a minimal covering set of legal markings and a minimal covered set of first-met bad markings (FBM) are computed. At each iteration, an FBM from the minimal covered set is selected. By solving an integer linear programming problem, a place invariant is designed to prevent the FBM from being reached and no marking in the minimal covering set of legal markings is forbidden. This process is carried out until no FBM can be reached. In order to make the considered problem computationally tractable, binary decision diagrams (BDD) are used to compute the sets of legal markings and FBM, and solve the vector covering problem to get a minimal covering set of legal markings and a minimal covered set of FBM. Finally, a number of FMS examples are presented to illustrate the proposed approaches. Yufeng Chen 0001, Zhiwu Li 0001, Mohamed Khalgui, Olfa Mosbahi |
IEEE Trans Autom. Sci. Eng. | 4 |
| 2011 | Reconfigurable Multiagent Embedded Control Systems: From Modeling to ImplementationabstractThe paper deals with reconfigurable embedded control systems following different component-based technologies and/or Architecture Description Languages used today in industry. We define a Control Component as a software unit to support control tasks of the system, which is assumed to be a network of components with precedence constraints. We define an agent-based architecture to handle automatic reconfigurations under well-defined conditions by creating, deleting, or updating components to bring the whole system into safe and optimal behaviors. To cover all possible reconfiguration forms, we model the agent by nested state machines according to the formalism Net Condition/Event Systems (NCESs), which is an extension of Petri nets. In addition, we apply a model checking to verify functional and extra-functional properties according to the temporal logic "Computation Tree Logic” (CTL). The goal is to check the agent reactivity after any evolution of the environment. Several complex networks can implement the system, where each one is executed at a given time when a corresponding reconfiguration scenario is automatically applied by the agent. To check the correctness of each one of them, we apply in several steps a refinement-based approach that automatically specifies feasible Control Components according to NCES. The model checker SESA is automatically applied in each step to verify deadlock properties of new generated components, and it is manually used to verify CTL-based properties according to user requirements. We implement the reconfiguration agent by three modules that allow interpretations of environment evolutions, decisions of useful reconfiguration scenarios, and finally, their applications. Two Industrial Benchmark Production Systems FESTO and EnAS available in our research laboratory are applied to explain the contributions of the paper. Mohamed Khalgui, Olfa Mosbahi, Zhiwu Li 0001, Hans-Michael Hanisch |
IEEE Trans. Computers | 2 |
| 2011 | A Component-Based Approach for the Development of Automated SystemsabstractThis paper addresses a component-based approach using the Event-B method to develop automated systems. These systems are composed of two parts: the control part (controller) and the operative part (controlled component). The first is a software component which controls the operative part that models the physical device and its environment. We propose in this paper the use of the formal Event-B method to develop automated systems applying a codesign technique, where the two components are developed separately, and then, a composition is defined with the Event-B method to prove the automated system correctness. First of all, we define a specification for the composition of these two components in the Event-B method. Second, we give refinement semantics for a component-based system before proposing a method to verify the refinement of a whole system from that of its components. Olfa Mosbahi, Mohamed Khalgui, Hans-Michael Hanisch, Zhiwu Li 0001 |
IEEE Trans. Syst. Man Cybern. Part A | 1 |
| 2010 | Intelligent distributed control systems
Mohamed Khalgui, Olfa Mosbahi |
Inf. Softw. Technol. | 2 |
| 2009 | Implementation of agent-based reconfigurable embedded control systemsabstractThe paper deals with the implementation of reconfigurable embedded control systems following the Component-based International Industrial Standard IEC61499, in which a Function Block is an event triggered software component owning data and an application is a composition of blocks. To handle automatic reconfigurations of the whole system, we define an agent-based architecture such that the agent checks and interprets the environment evolution before creates, updates or deletes Function Blocks according to well-defined conditions. It is composed of three modules: the interpreter that interprets the environment evolution, the engine that decides new reconfigurations according to such evolution and the converter that applies agent decisions. A Benchmark Production System is used to explain our contribution, and technical solutions are proposed to implement its different agent modules. Mohamed Khalgui, Olfa Mosbahi, Hans-Michael Hanisch |
INDIN | 2 |
| 2008 | A formal approach to check and schedule reconfigurable embedded control systemsabstractThis paper deals with the development of reconfigurable control systems following the component-based International Industrial Standard IEC61499. In this standard, a function block is an event-triggered component owning data and an application is a FB network that has to satisfy temporal properties. This network is totally changed or modified if a reconfiguration scenario is applied at run-time. We classify at first time all possible reconfiguration forms and we propose thereafter an Agent-based architecture to handle them. To verify temporal properties on the FB network corresponding to each reconfiguration scenario, we analyze the schedulability of the corresponding blocks. If it is feasible, then a static scheduling is generated as a sequencing to be used by the OS when the Agent applies at run-time the corresponding scenario. We deduce finally the whole system feasibility if the FB network corresponding to each possible scenario is feasible. A tool X - Reconfig is developed in our research laboratory to support the paper contribution. Mohamed Khalgui, Olfa Mosbahi, Hans-Michael Hanisch |
ETFA | 2 |
| 2006 | Formal development method of control systems using the event-based B approach Case study : A parcel sorting deviceabstractThis paper presents a formal method for the development of control systems. We aim at developing a program controlling the operative part of a control system. We first build an abstract model of the operative part and complete this model to get a model of the control system. The elements introduced to change the abstract model of the operative part to the automated system forms the controller of the automated system. The next steps consists in refining the abstract model to get a model of the operative part capturing every important feature. The method is developped through a case study : a parcel sorting system. Olfa Mosbahi, Jacques Jaray, Leila Ben Ayed |
AICCSA | 1 |
| 2002 | A Specification and Validation Technique Based on STATEMATE and FNLOG
Olfa Mosbahi, Leila Ben Ayed, Samir Ben Ahmed, Jacques Jaray |
ICFEM | 1 |