Leila Ben Ayed

dblp:j/LeilaJemniBenAyed · also Leila Jemni Ben Ayed, Leila Jemni BenAyed · DBLP profile ↗
← Back
52ranked-venue papers
3as first author
14since 2021 · last 2026
0000-0002-6031-7216ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Applied, interdisciplinary, general and emerging computing · 31 · 1 first-author · 5 since 2021Software engineering, systems software and programming languages · 27 · 3 first-author · 8 since 2021Human-computer interaction and ubiquitous computing · 11Artificial intelligence and machine learning · 4 · 4 since 2021Databases, data management, data science and information retrieval · 3Computer networks · 1Security and privacy · 1Graphics, computer vision, multimedia, augmented reality and games · 1 · 1 since 2021
YearPublicationVenuePosition
2026 An AI-Based Adaptive Workflow Model for Early Detection of Alzheimer's Disease
Nadine Mili, Sarra Abidi, Leila Ben Ayed
ENASE (1)3
2026 A Hybrid Lempel-Ziv-Welch Based Approach for Lossless-Lossy Color Image Compression Scheme
Taif Ammash, Hamza Gharsellaoui, Leila Ben Ayed
ICAART (5)3
2026 Self-Healing OCR Pipelines: A Modular Defense Framework against Visual and Semantic Attacks
Eya Ben Hmida, Sarra Abidi, Leila Ben Ayed
ICAART (5)3
2025 LICA-HE: Optimal Lossless Image Compression Algorithm for Color Passport-Photo Compression
Taif Ammash, Hamza Gharsellaoui, Leila Ben Ayed
ENASE3
2025 An Advance Facial Biometric Based System for Lossless Image Compression Algorithm
abstract
Recent interest has been generated in multimodal biometrics technology due to its potential to increase recognition rates by over- coming some of the fundamental limitations of single biometric modalities. The importance of different data compression algo- rithms is highlighted in the process of storing big data in data warehouses and archives and in reducing the volume of big data during its transmission through communication channels, so many compression algorithms have emerged that are designed to process different data. Images are used in different fields in our daily lives, such as social networks, medical diagnoses, remote sensing, and other fields, and since the size and accuracy of images are constantly evolving, the issue of storing and transferring images requires a compressing process to reduce their size. Although many approaches in data compression have been developed to alleviate these challenges, more efforts are still needed, especially for lossless image compression, which is a promising technique when critical information loss is not allowed. In this paper, we propose a new algorithm called the Lossless Image Compression Algorithm using a Column Subtraction model (LICA-CS). LICA-CS is efficient, low in complexity, decreases the image bit-depth, and enhances state-of-the-art performance. LICA-CS first implements a color transformation method as a pre-processing phase, which strategically minimizes inter-channel correlations to optimize compression outcomes. After that, a novel subtraction method was developed to compress the image data column-wise. We tackle the similarity and proximity of pixel values within adjacent columns, which offers a distinct advantage in reducing image size observing a significant size reduction of 71%. This is achieved through the subtraction of neighboring columns. The conducted experiments on colored images show that LICA-CS outperforms existing algorithms in terms of compression rate. Moreover, our method exhibited remarkable enhancements in execution time, with compression and decompression processes averaging 1.93 seconds. LICA-CS advances the state-of-the-art in lossless image compression, promising enhanced efficiency and effectiveness in image compression technologies
Taif Ammash, Hamza Gharsellaoui, Leila Ben Ayed
KES3
2024 A Tool-Supported Approach for Modelling and Verifying MapReduce Workflow Using Event B and BPMN2.0
Mayssa Bessifi, Ahlem Ben Younes, Leila Ben Ayed
ICSOFT3
2023 Adaptive user interface based on accessibility context
Lamia Zouhaier, Yousra Bendaly Hlaoui, Leila Ben Ayed
Multim. Tools Appl.3
2022 An Approach for the Specification and Verification of Hadoop-MapReduce Workflow
abstract
The growing importance of big data applications calls for the development of tools and methods to facilitate the development of high-quality applications. In this paper, we propose a model-driven approach for the specification and formal verification of the Hadoop-MapReduce workflow using the de facto standard BPMN2 and the Event B formal method. This approach is automated by the development of a prototype tool called BPMN-MapRed2EventB.
Mayssa Bessifi, Ahlem Ben Younes, Leila Ben Ayed
COMPSAC3
2021 A reactive system for specifying and running flexible cloud service business processes based on machine learning
abstract
In this paper, we present a reactive system for running flexible business process. We define two flexibility patterns based on BPMN (Business Process Model Notation) that deals with changes of resource requirements for business process. The business processes are built on an abstract level, using a BPMN model for the specification of the cloud service business process structure based on flexibility patterns, and the state-chart diagram for the specification of the cloud service business process behaviour. In fact, our approach is based on model driven engineering to facilitate the business process design for developers and free them from the lower cloud details during the running time of such applications. Moreover, the use of flexibility actions ensures the capacity of making a compromise between adapting rapidly and easily business process when running errors occur and keeping the effectiveness of these updated application models. This update is controlled by the real time system which is based on a machine learning algorithm to depict the appropriate cloud service to involve in the business process model using the right flexibility action. Finally, we present some results of our system.
Imen Ben Fraj, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC3
2021 HIR: A Hybrid IR Ranking Model
abstract
The aim of information retrieval (IR) process is to respond effectively to user queries by retrieving information that are better meets their expectations. A gap could exist between user information needs and his/her defined context as the level of the user's expertise in the search domain is directly influencing the query richness. The information retrieval system (IRS) must be intelligent enough to identify information needs and respond effectively to meet the expected needs, regardless the level of user's expertise level. This process is difficult and it remains a major and open challenge in the domain of IR. IR models integrate many sources to achieve an effective retrieval system. Semantic IR is an environment in which semantic techniques were applied to sort the documents according to their degree of relevance to the query. The present work proposes a hybrid model to rank documents. The proposed model is based on a query likelihood language model and the semantic similarity between concepts to assess the relevance between query-document pairs. Concepts were extracted by projection on WordNet ontology then word sense disambiguation was conducted. A semantic index was built to validate the proposed model. The conducted empirical experiments show that the proposed model is outperformed the compared benchmarks in the measured IR metrics.
Sameh Neji, Tarek Chenaina, Abdullah M. Shoeb, Leila Ben Ayed
COMPSAC4
2021 A Reinforcement Learning Based Approach of Context-driven Adaptive User Interfaces
abstract
Adaptive User Interfaces (AUI) have to exploit Artificial Intelligence powerful to adapt User Interfaces (UI)s to People With Disabilities (PWD). Thus, Machine Learning methods could master disabilities problems and barriers. In this paper, we propose a Reinforcement Learning (RL) based approach for resolving and surmounting PWD-UI interactions barriers since RL is good for learning good behavior. Hence, we have called the approach as RL-AUIAC as Reinforcement Learning of Adaptive User Interfaces for Accessibility Context. RL-AUIAC is based on three Knowledge Layers (KL)s depending on the kind of adaptation and the resolved problem at each layer. KL uses the Exploration-Exploitation dilemma to respond to the question: what to learn from each planned-adaptation sequences? In fact, Disability Knowledge Layer (DKL)learns UI structure behavior depending on the disability profile. Modality Knowledge Layer(MKL) learns facilities of adaptation on the basis of the couple. Platform Knowledge Layer (PKL) explores-exploits platform-knowledge to learn adaptation facilities on the basis of.
Lamia Zouhaier, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC3
2021 SemApp: A Semantic Approach to Enhance Information Retrieval
Sameh Neji, Tarek Chenaina, Abdullah M. Shoeb, Leila Ben Ayed
ICCSA (3)4
2021 A Specific Language for Developing Business Process by Refinement based on BPMN 2.0
Salma Ayari, Yousra Bendaly Hlaoui, Leila Ben Ayed
ICSOFT3
2021 HyRa: An Effective Hybrid Ranking Model
abstract
Information retrieval (IR) systems are concerned of the processing of the textual content of the document, the query, and issues of system effectiveness. IR models are means to integrate many sources of evidence on documents to achieve an effective retrieval system. Unlike traditional parameters such as word frequency in documents, semantic information retrieval is an environment that requires the application of semantic techniques. These techniques calculate a degree of query-document relevance to assign the highest rankings to the documents which are semantically closer to the query. To meet the user’s information needs and to optimize the performance of IR system, an innovative model was proposed to calculate the relevance of query-document pairs. The proposed model is a hybrid one that based on a query likelihood language model and a conceptual weighting model. It exploits the semantic similarity between document and query concepts and some document/collection statistics. The conducted experiments on the proposed model show improvement of the standard performance measures over the benchmark competitors. A statistical significance test is conducted to exclude the performance random variation of the compared models. Paired t-tests show that the proposed model is highly significant improves the most important measures.
Sameh Neji, Tarek Chenaina, Abdullah M. Shoeb, Leila Ben Ayed
KES4
2020 A control system for managing the flexibility in BPMN models of cloud service workflows
abstract
In this paper, we present a real time interactive system for running flexible workflow applications. This system facilitates the execution of these applications in terms of time execution complexity as it is based on flexibility mechanism. These workflows are built on an abstract level, through BPMN models using flexibility patterns. We define two flexibility patterns based on BPMN (Business Process Model Notation) that deals with changes of resource requirements for workflows. The provided models specify the functional view of workflows, whereas, their behavioral view is described using state-chart diagrams. A state-chart diagram represents the model specifying our real time system which controls the execution of workflow applications by making decisions on the use of flexibility actions. This execution is supported by the BPEL4WS engine that we have amended to execute flexible workflows and to be controlled by our real time system. Finally, we present some results of evaluations of our system.
Imen Ben Fraj, Yousra Bendaly Hlaoui, Leila Ben Ayed
CLOUD3
2019 A Grammar Based Approach to BPMN Model Semantic Preservation using Refinement
abstract
In this paper we introduce a description mechanism for specifying the refinement approach for Business Process Modeling and Notations(BPMN). We present at each level of abstraction the syntax of this BPMN models by a context-free grammar. After that, for each refined BPMN, we analyze, automatically the change impact using NuSMV model checker. The change impact concerns the semantic preservation of BPMN models during the refinement process.
Salma Ayari, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC (2)3
2019 From BPMN2 to Event B: A Specification and Verification Approach of Workflow Applications
abstract
The BPMN2 language suffers from the absence of a precise formal semantics of the various notations used, which often leads to ambiguities. In addition, this language does not have a proof system that validates a BPMN2 specification. Consequently, the use of a formal method, such as Event B, is a solution for dealing with the shortcomings found in the BPMN2 language. We propose in this paper a model-driven approach based on meta-model and meta-model transformation implemented in KerMeta to specify and formally verify workflows.
Ahlem Ben Younes, Yousra Bendaly Hlaoui, Leila Ben Ayed, Mayssa Bessifi
COMPSAC (2)3
2018 A New Approach for the Verification of BPMN Models Using Refinement Patterns
abstract
Modeling complex workflow systems, using BPMN (Business Process Modeling Notation), is quite a hard task that cannot be done in one step. The step-wise refinement technique facilitates the understanding of complex systems by dealing with the major issues before getting involved in the details. The proposed approach allows an incrementally developing of more and more detailed models with preserving the correctness of BPMN refined models at each step. Hence, we provide a formal semantics for BPMN models based on Kripke structure and BPMN refinement patterns to provide formal verification of this correctness. This verification is ensured automatically by NuSMV model Checker based on a BPMN language to NuSMV language transformation. The refinement correctness are expressed as refinement safety properties specified with LTL (Linear Temporal Logic).
Salma Ayari, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC (1)3
2018 A Refinement based Verification Approach of BPMN Models using NuSMV
Salma Ayari, Yousra Bendaly Hlaoui, Leila Ben Ayed
ICSOFT3
2017 A Model Driven Approach for Modelling and Running Flexible Cloud Service Workflows
abstract
Cloud computing is a new model for deploying and executing flexible workflow composed of cloud services. One of the expected facilities of Cloud environments is flexibility at different levels. In this paper, we propose a Model-Driven Approach (MDA) for the specification and the execution of cloud service flexible workflow applications. We define two flexibility patterns based on BPMN(Business Process Model and Notation) that deals with changes of resource requirements for workflow. The workflows are built on an abstract level, using a BPMN model for the specification of the cloud service workflow structure based on flexibility patterns, and the state-chart diagram for the specification of the cloud service workflow behavior. The execution process is supervised by a control system which is responsible for making decisions on the execution of the workflow based on the behavior of the engine defined by the state-chart diagram.
Imen Ben Fraj, Yousra Bendaly Hlaoui, Leila Ben Ayed
AICCSA3
2017 A Modeling Approach for Flexible Workflow Applications of Cloud Services
abstract
In this paper we propose an model driven approach for the specification and the execution of flexible workflows composed from cloud services. Flexibility of workflow means fast reactivity to internal and external changes. The basic challenge for workflow now is the ability to respond dynamic changes. To fulfill, we define functional and behavioral views of the flexible workflow. The first view is modeling by BPMN language and the other by a the statechart model. Besides, we describe how the workflow reacts to dynamic changes. To be executed, workflow models should be translated into BPEL4WS language which will be executed by the BPEL4WS engine, the later is driven by the behavior described by the statechart model. In addition, we present an execution infrastructure suitable for the execution of flexible workflows.
Imen Ben Fraj, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC (2)3
2017 Cloud Adapted Workflow e-Assessment System: Cloud-AWAS
abstract
In this paper, we present an approach to adapt the e-assessment workflow by considering learner's profiles. We have started by creating a learner profile ontology based on extraction data from e-assessment activities, file log and personal information. Then, we have defined three adaptation actions: Add Activity, Edit Activity and Delete Activity, applied on the workflow assessment and using information extracted from learner profile ontology instances. Each action is applied according to conditions. After that, we present some results of the empirical evaluation of our system.
Fahima Hajjej, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC (1)3
2017 From Sequence Diagrams to Event B: A Specification and Verification Approach of Flexible Workflow Applications of Cloud Services Based on Meta-model Transformation
abstract
This paper presents a meta-model transformation based approach to reasoning about sequence diagrams using B event. We present an approach for the specification and the verification of flexible Workflow applications of cloud services. Our approach is based on the semiformal notation of UML sequence diagrams, and the formal method B event. We have developed a tool called SD2EventB supporting the proposed approach. This tool allows the specification of flexible Cloud service Workflow application models using predefined flexibility patterns generated automatically by this tool. Once the model is specified, it is transformed to an event B model to be verified. In order to ensure this verification, we have used the platform Rodin supporting the event B method. This platform has been integrated into our tool. The transformation, as well, has been developed as a function of our tool using the meta-model transformation environment KerMeta.
Yousra Bendaly Hlaoui, Ahlem Ben Younes, Leila Ben Ayed, Manel Fathalli
COMPSAC (2)3
2017 Users Interfaces Adaptation for Visually Impaired Users Based on Meta-Model Transformation
abstract
We apply the Model-Driven Engineering for adapting User Interfaces (UI) in order to improve their accessibility into interactive system (IS). The solution that we propose has to be generic to be applicable in any context and with any type of UI. Therefore, we have developed a model driven approach based on meta-model transformations. This approach generates modality-based UI models adapted to each kind of disability. Hence, we have developed an accessibility context described with the type of disability, the used platform, the user identity, his/her situation and the surrounded environment. This context is defined with an ontology which will be used in the adaptation process. To generate Platform Independent and Specific UI Models, we have proposed a set of metamodel transformation rules.
Lamia Zouhaier, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC (1)3
2017 Adapted E-Assessment System Based on Cloud Computing
abstract
Using Cloud Computing environment, the e-assessment process becomes an orchestration of a set of dedicated cloud services. In this paper, we propose an architecture for an e-assessment environment based on cloud services. This environment implements an approach that we have proposed to develop a generic e-assessment process which will be adapted to a learner profile. The e-assessment process activities and the adaptation process are implemented as Cloud services. Furthermore, they could be invoked from any existing Learning Management System (LMS).
Fahima Hajjej, Yousra Bendaly Hlaoui, Leila Ben Ayed
ICALT3
2017 A Smart Educational Game to Model Personality Using Learning Analytics
abstract
Various research work have highlighted the importance of modeling learner's personality to provide a personalized computer based learning. In particular, questionnaire is the most used method to model personality which can be long and not motivating. This makes learners unwilling to take it. Therefore, this paper refers to Learning Analytics (LA) to implicitly model learners' personalities based on their traces generated during the learning-playing process. In this context, an LA system and an educational game were developed. Forty five participants (34 learners and 11 teachers) participated in an experiment to evaluate the accuracy level of the learners' modeling results and the teachers' satisfaction degree towards this LA system. The obtained results highlighted that the LA system has a high level of accuracy and a "good" agreement degree compared to the questionnaire paper. Besides, the teachers found the LA system easy to use, useful and they were willing to use it in the future.
Ahmed Tlili, Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni, Kinshuk
ICALT3
2016 A Generic E-Assessment Process Development Based on Reverse Engineering and Cloud Services
abstract
Nowadays, there are many problems related to the e-learning in the development of E-assessment such as the difficulty to use the assessment object from a platform to another one. As the domain model reuse rate is very low in various e-learning systems and hardness to guarantee the consistency between designs and codes. Therefore, we need an approach aiming to generate a general process of the e-assessment. The present study describes an approach for integrating e-assessment functionalities of learning management systems (LMS) candidates into a generalized e-assessment process. To attempt these goals, we have studied different existing LMSs to depict their various e-assessment activities from which we have generated a set of generic e-assessment activities using the reverse engineering. Then, we have integrated these activities into a workflow model to specify a generic e-assessment process based on pedagogical scenarios. We have defined these scenarios using workflow to provide an abstract e-assessment process. Finally, we have implemented this generic e-assessment workflow as a cloud computing service to be invoked from any LMS.
Fahima Hajjej, Yousra Bendaly Hlaoui, Leila Ben Ayed
CSEE&T3
2016 Towards a Generic UML Model to Support Designing Educational Role Playing Games
abstract
Recently, educational games are gaining increasing attention from researchers and practitioners in the learning field. This is because they are fun, motivating and immersive. However, designing educational games can be difficult for people who do not have appropriate background towards game development. This is further complicated by the fact that there are many genres of games (role playing, action, puzzle, etc.) and each genre has its own game elements and functionalities. This makes the game design process confusing, especially for beginners. This paper deploys the powerful graphical representation of Unified Modeling Language class diagram to present a generic model of educational role playing games. This model uses knowledge representation (game elements, functionalities and features) to support designing educational role playing games. Fifty eight game developers participated in evaluating the model and they have revealed its high perceived usefulness while designing educational role playing games. In addition, they reported that they were willing to use this model again in the future in their context.
Ahmed Tlili, Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni, Kinshuk
ICALT3
2015 A Model Driven Approach for Design Flexible e-Assessment
abstract
Currently, there are many problems in the domain of the development of the e-Assessment process such as the difficulty to use a same e-assessment process by different e-learning platforms, the low rate of the e-assessment model reuse by various e-learning systems and the hardness to guarantee the consistency between designs and codes. Therefore, to resolve these problems, we need an approach aiming to develop a generic e-assessment process model which will be adapted automatically to any e-learning system. Hence, we propose a model driven approach for design flexible E-assessment process. We use an abstract description provided by UML activity diagram language and coupled with LTSA standards.
Fahima Hajjej, Yousra Bendaly Hlaoui, Leila Ben Ayed
CSEDU (1)3
2015 Using Cloud Computing for E-assessment Process Integration
abstract
Currently, there are many problems of the application development of E-Assessment such as the difficulty to use the assessment object from a platform to another one. In addition, the domain model reuse rate is very low in various application systems, and hardness to guarantee the consistency between designs and codes. Therefore, to resolve these problems, we need an approach aiming to automate the modeling and coding processes in e-assessment system. The present study describes an approach, based on service cloud computing, for integrating e-assessment functionalities of candidate LMS systems into a generalized e-assessment process.
Fahima Hajjej, Yousra Bendaly Hlaoui, Leila Ben Ayed
EC-TEL3
2014 Generating Accessible Multimodal User Interfaces Using MDA-Based Adaptation Approach
abstract
In order to ensure accessibility of user interface, it is highly recommended to elaborate a generic solution which is compliant to disable user requirements and best accommodates their particular needs. Therefore, we propose, in this paper, a generic MDA-based solution of adapting application's interface to accessibility context. It consists of generating, automatically, accessible adapted User Interfaces. Hence, we propose a multimodel approach by incorporating the modality of interaction into adaptation process. Consequently, based on MDA principals, we develop different meta-model transformations to provide an adapted User Interface model according to recent accessibility context information and a given non adapted User Interface.
Lamia Zouhaier, Yousra Bendaly Hlaoui, Leila Ben Ayed
COMPSAC3
2014 A Proof of the Correctness of a Transformation Approach from UML Activity Diagrams to Event-B Models
abstract
We propose a workflow application constructive approach in which Event B models are built incrementally from UML AD models. Following our proposed approach, to be verified, workflow activity diagram models should be translated into Event B models which will be proved using the RODIN tool. To reach this objective, we propose, in this paper, a meta-model based transformation from UML AD to Event B models. To ensure the correctness and the completion of the transformation we propose a graph homomorphic mapping between the activity diagram and Event B models elements. By an example of workflow application we illustrate the proposed technique.
Ahlem Ben Younes, Yousra Bendaly Hlaoui, Leila Ben Ayed
iiWAS3
2013 Automatic Generation of UIs for Disabled Users using Context-aware Techniques and Reasoning
Lamia Zouhaier, Yousra Bendaly Hlaoui, Leila Ben Ayed
KEOD3
2013 Towards a Formal Semantic for UML 2.0 - Activity Diagram based on Institution Theory
Amine Achouri, Leila Ben Ayed
ICSOFT2
2011 Evaluation of Personalization Strategies Based on Fuzzy Logic
abstract
Teachers and course authors need to apply various instructional strategies in order to personalize their courses. It is not a trivial task and the time, the efforts and the learning objects needed for preparing personalized learning scenarios depend on the personalization strategy to be applied. This paper presents an approach for selecting appropriate personalization strategies according to the feasibility of generating personalized learning scenarios with minimal burden on the author. Two metrics are proposed for putting in order and selecting useful personalization strategies. The calculation of these metrics is automated based on the analyses of the Learning Object Metadata (LOM) standard according to the semantic relations between data elements and learners' characteristics.
Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni, Kinshuk, Sabine Graf
ICALT2
2011 An UML _AD-to-event_B refinement based approach for specifying and verifying workflow applications
abstract
In this paper, we propose an approach for the specification and the verification of workflow applications using UML AD and Event B. Workflow carries applications where many actors take part and cooperate in order to execute operations. Upon composing those operations, many problems such as deadlock, freeness and livelock might appear. In this context, we are going to show how to express an UML Activity Diagram model in Event B. In our approach, the workflow is initially expressed incrementally graphically with UML AD, then translated into Event B and verified using the B powerful support tools. The Event-B expression of the UML AD model allows us to give it a precise semantics. We propose a workflow applications constructive approach in witch Event B models are built incrementally from UML AD models, driven by UML refinement patterns. The use of the B formal method and its refinement mechanism allows the verification of the correction of the UML AD refinement patterns.
Ahlem Ben Younes, Leila Ben Ayed
iiWAS2
2011 A formal approach for the development of reactive systems
Olfa Mosbahi, Leila Ben Ayed, Mohamed Khalgui
Inf. Softw. Technol.2
2010 An Ontology Based Approach for Selection of Appropriate E-learning Personalization Strategy
abstract
When there are many possible personalization strategies, it is important to select the most appropriate of them according to the specificities of the course. In this context, rises the contribution of this work, which is the analysis of learning objects as well as the metadata describing them for the selection of appropriate personalization strategy.
Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni
ICALT2
2010 An UML Activities Diagrams Translation into Event B Supporting the Specification and the Verification of Workflow Application Models - From UML Activities Diagrams to Event B
Leila Ben Ayed, Najet Hamdi, Yousra Bendaly Hlaoui
ICSOFT (2)1
2010 Using AToM3 for the Verification of Workflow Applications
Leila Ben Ayed, Ahlem Ben Younes, Amin Ben Brahim Achouri
ICSOFT (2)1
2010 Specification and Verification of Workflow Applications using a Combination of UML Activity Diagrams and Event B
Ahlem Ben Younes, Leila Ben Ayed
ICSOFT (2)2
2008 From AUML Protocol Diagrams to Event B for the Specification and the Verification of Interaction Protocols in Multi-agent Systems
abstract
This paper presents a new event-B based approach to reasoning about interaction protocols. We show how an event-B model can be structured from AUML protocol diagrams and then used to give a formal semantic to protocol diagrams which supports proofs of their correctness. More precisely, we give rules for the translation of protocol diagrams into event-B language. In particular, we focus on the translation of messages with response delay. The event-B language allows the definition of invariant describing required interaction properties and provides an automatic proof. By an example of multi-agent systems interaction protocol, we illustrate the proposed translation.
Leila Ben Ayed, Fatma Siala
COMPSAC1
2008 From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications
abstract
This paper presents a new event-B based approach to reasoning about workflow applications. We show how an event-B model can be structured from UML Activity diagrams (UML AD) and then used to give a formal semantic to UML AD which supports proofs of their correctness. More precisely, we give rules for the translation of UML AD into event-B language. In particular, we propose a solution that uses the refinement in Event B to encode the hierarchical decomposition of activities in UML AD. The event-B method allows the definition of invariant describing required properties (deadlock-inexistence, liveness, fairness) and provides an automatic proof. We discuss the contributions and by an example of a workflow application, we illustrate the proposed approach.
Ahlem Ben Younes, Leila Ben Ayed
COMPSAC2
2008 Extended UML activity diagram for composing Grid services workflows
abstract
This paper focuses on how to model and compose workflow applications of Grid services without considering lower level description of the Grid environment. To reach this objective, we propose a model-driven approach (MDA) for developing workflow applications from existing Grid services. The workflows are built on an abstract level with semantic and syntactic descriptions of services available on the Grid using UML activity diagram language. As there are particular needs for modeling composed workflows of Grid services, we propose to extend the UML activity diagram notation. These extensions deal with additional information allowing a systematic composition of workflows and containing appropriate data to describe a Grid service. These data are useful for the execution of the resulting workflow.
Yousra Bendaly Hlaoui, Leila Ben Ayed
CRiSIS2
2008 UML Class Diagram as a Navigational Support for E-Learning
abstract
Several researches have demonstrated the effectiveness of graphical languages in knowledge representation and the numerous advantages of using graphs in the context of learning. On the other hand, many researches in the e-learning domain have focused on the personalization of learning materials by using adaptive educational hypermedia. However, most adaptive educational hypermedia systems do not benefit from the power of graphics because they do not use an expressive graphical language for presenting educational hypermedia to the learners. Our approach fills the existing gap between current educational hypermedia languages with the learnerspsila requirement of a standard graphical language for the visualization of adaptive hypermedia and the navigation through it. In this way, new possibilities are added to adaptive hypermedia expressiveness such as the presentation of the relations between concepts and the organization of these concepts in compartment allowing the arrangement of their semantics.
Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni, Kinshuk
ICALT2
2008 Event-B based invariant checking of secrecy in group key protocols
abstract
The correctness of group key protocols in communication systems remains a great challenge because of dynamic characteristics of group key construction as we deal with an open number of group members. In this paper, we propose a solution to model group key protocols and to verify their required properties, in particular secrecy property, using the event-B method. Event-B deals with tools allowing invariant checking, and can be used to verify group key secrecy property. We define a well-formed formal link between the group protocol model and the event-B counterpart model. Our approach is applied on a tree-based group Diffie-Hellman protocol that dynamically outputs group keys using the logical structure of a balanced binary tree.
Amjad Gawanmeh, Sofiène Tahar, Leila Ben Ayed
LCN3
2007 Using UML Activity Diagrams and Event B for Distributed and Parallel Applications
abstract
This paper presents a specification and verification technique for distributed and parallel applications using formal and semi-formal methods. The proposed technique uses UML and Event B. The design is initially expressed graphically with UML, then translated into Event B and verified using the B powerful support tools. In this paper, we focus on the translation of activity diagrams into Event B, in order to verify workflow properties of distributed and parallel applications with the B prover. We present translation rules of activity diagrams into Event B, and relation between hierarchical decomposition of activities in UML activity diagrams and the refinement in Event B.
Ahlem Ben Younes, Leila Ben Ayed
COMPSAC (1)2
2007 A Multi-Parameters Personalization Approach of Learning Scenarios
abstract
In this paper, we present an approach for the personalization of learning scenarios integrating different personalization parameters. In addition to "classical" ones such us learner preference, learning style, learner motivation and learner background, we integrate another aspect of personalization which focuses on the pedagogical approach. In fact, the context of learning, as well as the personalized object (contents and activities) and the personalization parameters depends strongly on the pedagogical approach.
Fathi Essalmi, Leila Ben Ayed, Mohamed Jemni
ICALT2
2006 Formal development method of control systems using the event-based B approach Case study : A parcel sorting device
abstract
This 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
AICCSA3
2006 Graphical UML View from Extended Backus-Naur Form Grammars
abstract
This paper addresses the graphical representation of Context-Free Grammars (CFG) written in extended Backus- Naur Form (EBNF), using UML class diagrams. These diagrams can help understand the grammar for users who are not familiar with concepts of EBNF grammars. The additional structure afforded by UML could help to clarify how the derived language is constructed and allows learner to build significance relations between the concepts presented. We propose derivation rules of EBNF grammars into UML class diagrams which will be illustrated over an example of a grammar written in EBNF.
Fathi Essalmi, Leila Ben Ayed
ICALT2
2005 Introducing Dynamic Properties with Past Temporal Operators in the B Refinement
Mouna Chaouch-Saad, Leila Ben Ayed
ATVA2
2002 A Specification and Validation Technique Based on STATEMATE and FNLOG
Olfa Mosbahi, Leila Ben Ayed, Samir Ben Ahmed, Jacques Jaray
ICFEM2