Institut Supérieur d'Informatique et de Mathématiques de Monastir

We provide a branch-and-price algorithm for the bin packing problem with conflicts, a variant of the classical bin packing problem that has major applications in scheduling and resource allocation. The proposed algorithm benefits from a number of special features that greatly contribute to its efficiency. First, we use a branching rule that matches the conflicting constraints, preserving the structure of the subproblems after branching. Second, maximal clique valid inequalities are generated based on the conflicting constraints and are added to the subproblems. The algorithm is tested on a standard set of problems and is compared to a recently proposed approach. Numerical results indicate its efficiency and stability.

The objective of vehicular communication is to improve road safety and traffic efficiency through a variety of cooperative intelligent transport system (C-ITS) services. These services allow information exchange between vehicles and other communication entities (e.g., vehicles, infrastructure, pedestrians). Many advanced services are envisaged to support autonomous vehicles and safety applications. The performance requirements of such services are considered highly critical for road safety. However, all these services increase the channel load, and thus, it is difficult to differentiate which service has a higher priority for accessing communication channels. In this paper, we focus on the classification of C-ITS services, which allows the cohabitation of all services considering the strict performance requirements for some services. The aim is to classify C-ITS services based on their packet delay requirements in order to define higher priority for critical services to ensure their dissemination, especially under congestion conditions. Then, we present protocols and quality of service (QoS) mechanisms that can map this classification to the available vehicular networks.

Cloud environments are being increasingly used for deploying and executing business processes to provide a high level of performance with low operating cost. Nevertheless, due to the lack of an explicit and formal description of the resource perspective in the existing business processes, the correctness of Cloud resources management can not be verified. The aim of the present work is to offer a formal definition of the resource perspective in business processes as a step towards ensuring a correct and consistent Cloud resource allocation in business process modeling. Concretely, we propose a formalism based on the Event-B language for specifying Cloud resource allocation policies in business process models. This formal specification is used to formally validate the consistency of Cloud resource allocation for process modeling at design time, and to analyze and check its correctness according to user requirements and resource capabilities. In order to show its feasibility, our approach has been tested using a real use case study from an industrial partner.

In the recent years, the wireless technology would have known an exponential growth, which has an impact on developing and improving the field of telecommunications beyond the means of transmission wire to the radio frequency communication. The Wireless Sensor Network (WSN) is enrolled in this context. It's a collection of component (nodes) organized into a cooperative network. The main components of this network are tiny battery powered cameras with wireless communication capability. Therefore, image transfer in WSNs presents major challenge which raises issues related to its representation, its storage and its transmission. However, communication of image content has several bottlenecks, including limited bandwidth of cellular networks, restricted computational power, limited storage capability, and battery constraints of the appliances. In this paper, we address the energy, system lifetime and bandwidth bottlenecks of image communication. We present an efficient adaptive compression scheme that can significantly minimize the energy required for wireless image communication while meeting bandwidth constraints of wireless network and image quality. Based on Discrete Wavelet Transform, we propose an efficient image compression scheme, enabling significant reduction in computation energy needed with minimal degradation of image quality. Simulation results are done with C++ and show that the proposed scheme optimizes network lifetime, reduces significantly the amount of required memory and minimizes both (i) computation energy, by reducing the computation needed to compress an image and (ii) communication energy, consumed by the RF component which is proportional to the number of transmitted bits.

Abstract Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.

A configurable process model captures a family of similar processes. Such models can be configured to obtain a process variant according to specific requirements. With this aim, several approaches have been proposed for the configuration of process models. Nevertheless, an increasing attention is being paid to achieve this in a sound manner due to the complex inter-dependencies between the configuration decisions. In this work, we aim to guide the process analyst to easily configure process models while preserving soundness. To do so, we propose a formal approach for ensuring correctness of business process configurations while considering structural constraints they have to obey. Specifically, using the Event-B language, we formally define a configurable process model, its correctness-preserving conditions and its configuration constraints.

Cloud environments are being increasingly used for deploying and executing business processes to provide a high level of performance with low operating cost. Nevertheless, due to the lack of explicit and formal description of the resource perspective in existing business processes, cloud resources cannot be efficiently and optimally managed. The aim of the present paper is to offer a formal definition of the resource perspective in business processes as a step towards ensuring correct and optimal Cloud resource allocation in business process modeling. Concretely, we propose a formalism based on the Event-B for specifying Cloud resource allocation policies in business process models. This formal specification is used to formally validate the consistency of Cloud resource allocation for process modeling at design time, and to analyze and check its correctness according to users needs and resource properties. In order to show its feasibility, our approach has been tested using a real use case study from an industrial partner.

Nowadays, a growing number of companies are using Cloud Computing to optimize their business processes by using dynamically scalable and often virtualized resources on demand. Nevertheless, due to the lack of explicit and formal description of the resource perspective in existing business processes, Cloud resource allocation behavior cannot be efficiently and correctly managed. In this paper, we aim at formally verifying resource allocation in business processes using Event-B. More precisely, our aim is to specify the resource allocation behavior both at design time and at runtime, and to check its correctness according to users' needs. Our model also takes into account different cloud properties such as elasticity and shareability. In order to show its feasibility, our approach has been tested using a use case study from an industrial partner.

The emerging technology during the last years allowed the development of new sensors equipped with wireless communication which can be organized into a cooperative autonomous network. Some application areas for wireless sensor networks (WSNs) are home automations, health care services, military domain, and environment monitoring. The required constraints are limited capacity of processing, limited storage capability, and especially these nodes are limited in energy. In addition, such networks are tiny battery powered which their lifetime is very limited. During image processing and transmission to the destination, the lifetime of sensor network is decreased quickly due to battery and processing power constraints. Therefore, digital image transmissions are a significant challenge for image sensor based Wireless Sensor Networks (WSNs). Based on a wavelet image compression, we propose a novel, robust and energy-efficient scheme, called Priority Image Transmission (PIT) in WSN by providing various priority levels during image transmissions. Different priorities in the compressed image are considered. The information for the significant wavelet coefficients are transmitted with higher quality assurance, whereas relatively less important coefficients are transmitted with lower overhead. Simulation results show that the proposed scheme prolongs the system lifetime and achieves higher energy efficiency in WSN with an acceptable compromise on the image quality.

Composite services often run in dynamically changing environments where new composition requirements can be added and Web services may disappear or their quality of service may decline. The service composition requirements are classified into three groups: functional, nonfunctional, and transactional requirements. The functional computing requirements concern functional capabilities of Web services. The nonfunctional computing requirements are defined as service-level agreements (SLA) constraints. The transactional computing requirements define behavioral constraints and are expressed by designers using the acceptable termination states (ATS) concept. In this work, we proposed an adaptive service composition (ASC) approach. Such an approach is adaptive as it can be used to either define or reconfigure composite services according to SLA and ATS constraints. It introduces a new recovery capability (RC) concept for capturing the recoverability level supported by Web services. We adopted a genetic-based algorithm to model the ASC approach. The choice of such an algorithm is justified by the nature of the problem of our ASC process which belongs to the NP-hard class. We experimentally showed the effectiveness of our ASC approach and empirically studied the service composition RC in particular.

Vehicular ad hoc network (VANET) routing protocols resort to clustering in order to optimize broadcast traffic flooding. Clustering schemes usually rely on rules which apply to each vehicle in order to reach a targeted organization in a VANET. Most of the literature works which evaluate clustering for VANET focus on performance analysis. However, with autonomous vehicles coming to roadways, more rigorous relationships will be required between clustering rules and the resulting organization, so as to anticipate road safety in a better way. We propose a formal description of the properties which are expected in a VANET, while considering the rules of a given clustering scheme. Using Event-B, we first present a description of the VANET, the vehicles movement and the traffic generated by both routing and application messages. Then, based on an Event-B model of a basic routing protocol of the literature, we describe how the specific rules of a clustering scheme can be modeled along with the properties expected in the resulting organization. Finally, we propose a validation process of the model. This paper aims at showing how our proposals have been applied to the Chain-Branch-Leaf scheme, although they can be adapted to any rule-based clustering scheme for VANET.

Service Component Architecture (SCA) is a set of specifications which describe a model for building applications and systems using a Service-Oriented Architecture (SOA). However, SCA in its current form does not represent any formal definition. In addition, there is a growing interest for verification techniques which help to prevent SCA composition specification failure. In this context, we intend to propose an Event-B based approach so as to configure the SCA composition dynamically. We focus, particularly, on the correctional dynamic such as substituting faulty services and components. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

With the emergence of Service Component Architecture (SCA), all interests were focused on representing this architecture in a formal way in order to be able to prevent the specifications failures. In this context, our recent works were interested in formalizing structural properties of the SCA specifications, particularly in defining structural compatibility between connected services. In fact, verifying structural compatibility is necessary but not sufficient. In this paper we intend to represent, in a first step, the SCA behavioral properties by means of Event-B invariants and events. In a second step, we established behavioral compatibility between services interacting together which is considered as a delicate task and has a great importance in guaranteeing reliable communication between services. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

In this paper, the performance of a new design of a piezoelectric Inertial Measurement Unit system (EMU) is evaluated through FEM simulations. This paper compares performance of a new proposed design with a previously reported one. The proposed sensor relies on Coriolis Effect for angular velocity detection and on direct piezoelectric Effect for acceleration measurements. This work addresses the detection improvement of both angular velocity and acceleration motions through a new proposed design. Compared to the reported design, the new structure produces an increase of 37.5% in the output voltage for a z-axis acceleration of 10 g. Similarly, for an angular velocity of 180 deg/s, an output voltage of 1 V is obtained from the new design compared to 200 mV from the reported one.

Formal methods such as B and Event-B support the achievement of correct systems design using the refinement technique. These methods allow for the description of data and actions at different levels of abstraction. The OCL provides some precision to UML models. The means offered by OCL Collection, Set, OrderedSet, Bag and Sequence are insufficient to support an incremental process of class diagrams development based on technical refinement. Indeed, the description of an initial model often requires very abstract mathematical concepts such as relation and function. These concepts are difficult to express in OCL using TupleType and def. This discourages the designer from expressing abstract constraints. Moreover, the absence of these concepts does not favor the move from semi-formal to formal: UML/OCL to Event-B. To overcome these flaws, we propose an OCL mathematical extension by increasing its class library.

Over the past few years, osteoarthritis is one of the most common knee diseases. The diagnosis and treatment of this disease is a vital importance. Furthermore, Deep Learning (DL) approaches have shown a good performance in learning the high-level features and in resolving segmentation issues. In this paper, we propose a new model of DL 3D-Res-UNet in order to accurately segment the knee cartilage from a Magnetic Resonance Imaging (MRI) 3D construction that allows perfectly visualizing the anatomical structure of this organ. This model is a combination of an architecture widely known in the literature for its segmentation efficiency (3D-UNet) with a residual architecture (3D-ResNet). The experimental results reveal that the suggested model can stabilize the training model, segment the cartilage from MRI very well and compete with the state of art on multiple performance metrics. The gain of precision and recall with 3DRes-UNet is given up to 15% and 26% compared to 3D-ResNet and 3D-UNet, respectively, hence the effectiveness of the suggested method.

The main issues for the fulfillment service level agreements (SLA) are concerned with problem of variability of QoS properties (vQoS). Indeed, the QoS properties may evolve frequently either because of internal changes or because of workload fluctuations. To solve the vQoS problem, we first introduced three variability operators: replicate, delete and replace. These operators will be used to reconfigure CWS when the SLA contract is violated. The first two operators are used to add and remove Web service instances, while the last one is used to substitute some faulty Web services. Then, we proposed an incremental approach for modeling and verifying the composites services (CWSs) reconfiguration using Event-B. We start by abstractly specifying the main requirements and then we refine them through several steps to model CWSs. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we used ProB model-checker to trace possible design errors. We have exploited the LTL for dynamic reconfigurations to characterize the correct behavior of CWSs reconfiguration.

In this paper, we propose a new ant based clustering algorithm. The algorithm takes inspiration from the sound communication properties of real ants. Artificial ants communicate directly with each others in order to merge similar group of objects. The proposed algorithm was tested and evaluated. The obtained results are very encouraging in comparison with the famous k-means and some ant based clustering algorithms.

The polyaniline was doped with sulfonic acid and functionalized with single‐walled carbon nanotubes. The effects of single‐walled carbon nanotubes (SWCNTs) inserting and thermal annealing at T = 393 K, during 24 h are carried out by optical and structural study. Structural characterizations of D‐polyaniline (PANI) or D‐PANI/SWCNTs compounds at both pristine and annealed states were obtained by Fourier Transform infrared analysis and scanning and transmission electron microscopies. Optical parameters including absorption coefficient, optical transition type, energy gaps, skin depth, and extinction coefficient have been also elucidated from optical absorption measurements. Moreover, the characteristics of the localized states introduced either by SWCNTs adding and/or annealing temperature are carried out. By referring to the starting material, the direct (indirect) optical band gap was found to be reduced from 3.91 (3.75) to 2.35 (2.24) eV, after SWCNTs inserting and annealing. Moreover, new localized states having a band width of 390 meV are created at 1.25 eV. The SWCNTS dispersion quality on the organic matrix and the PANI self‐crosslinking lead to the charge transfer and the resulting interpenetrating network can be used as active layers for organic solar cells. POLYM. COMPOS., 40:E821–E831, 2019. © 2018 Society of Plastics Engineers

This paper presents the design optimization of thermoelectric generators (TEGs) based on low temperature co-fired ceramic (LTCC) technology. Three designs, containing 45 Ag/Ni thermocouples each, were studied: two conventional designs (π-type and Y-type TEGs) and one newly proposed design. The optimization was carried out to improve the temperature difference along thermocouple (TC) arms by increasing thermal resistance of the structure and by increasing the temperature difference path with maintaining the same TC dimensions. For thermoelectric modules (TEMs) with 60 generators, the optimized TEG produces maximum electrical power of 1.7 W at ΔT <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">TEG</sub> = 230 °C while the π- and Y-type thermoelectric generators produces respectively maximum output power of 0.022 W and 1 W.