Article de revue avec comité de lecture (10)
BOSILCA George, BOUTEILLER Aurélien, GUERMOUCHE Amina, HERAULT Thomas, ROBERT Yves, SENS Pierre, DONGARRA Jack
A failure detector for HPC platforms. International journal of high performance computing applications (IJHPCA), january 2018, vol. 32, n° 1, pp. 139-158
URL: https://hal.inria.fr/hal-01453086/document
abstract
Building an infrastructure for exascale applications requires, in addition to many other key components, a stable and efficient failure detector. This article describes the design and evaluation of a robust failure detector that can maintain and distribute the correct list of alive resources within proven and scalable bounds. The detection and distribution of the fault information follow different overlay topologies that together guarantee minimal disturbance to the applications. A virtual observation ring minimizes the overhead by allowing each node to be observed by another single node, providing an unobtrusive behavior. The propagation stage uses a nonuniform variant of a reliable broadcast over a circulant graph overlay network and guarantees a logarithmic fault propagation. Extensive simulations, together with experiments on the Titan Oak Ridge National Laboratory supercomputer, show that the algorithm performs extremely well and exhibits all the desired properties of an exascale-ready algorithm
BOUZID Zohir, RAYNAL Michel, SUTRA Pierre
Anonymous obstruction-free (n,k)-set agreement with n−k+1 atomic read/write registers. Distributed computing, april 2018, vol. 31, n° 2, pp. 99-117
abstract
The k-set agreement problem is a generalization of the consensus problem. Namely, assuming that each pro- cess proposes a value, every non-faulty process must decide one of the proposed values, under the constraint that at most k different values are decided. This is a hard problem in the sense that it cannot be solved in a pure read/write asyn- chronous system, in which k or more processes may crash. One way to sidestep this impossibility result consists in weak- ening the termination property, requiring only that a process decides if it executes alone during a long enough period of time. This is the well-known obstruction-freedom progress condition. Consider a system of n anonymous asynchronous processes that communicate through atomic read/write reg- isters, and such that any number of them may crash. This paper addresses and solves the challenging open problem of designing an obstruction-free k-set agreement algorithm with only (n −k +1) atomic registers. From a shared memory cost point of view, our algorithm is the best algorithm known to date, thereby establishing a new upper bound on the number of registers needed to solve this problem. For the consensus case (k = 1), the proposed algorithm is up to an additive factor of 1 close to the best known lower bound. Further, the paper extends this algorithm to obtain an x-obstruction- free solution to the k-set agreement problem that employs (n − k + x) atomic registers (with 1 ≤ x ≤ k < n), as well as a space-optimal solution for the repeated ver- sion of k-set agreement. Using this last extension, we prove that n registers are enough for every colorless task that is obstruction-free solvable with identifiers and any number of registers
CHANE-YACK-FA Raphael , FRAPPIER Marc, MAMMAR Amel, FINKEL Alain
Parameterized verification of monotone information systems. Formal aspects of computing, august 2018, vol. 30, n° 3-4, pp. 463-489
abstract
In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states
LIAO Jianwei, TRAHAY François, CAI Zhigang, XIONG Hailing, CHEN Shanxiong, ISHIKAWA Yutaka
Fine granularity and adaptive cache update mechanism for client caching. IEEE systems journal, 2018, pp. 1-12 (document in press - published online 05 Sep 2018)
abstract
Distributed file systems have been commonly used as the back end to provide high-performance I/O services for hosting complicated data processing, such as database workloads. By buffering the frequently used data in the local file cache, which is called the client caching mechanism, can reduce the I/O latency and improve the performance of file access. However, the overhead and complexity for ensuring data consistency may offset the performance benefits caused by data caching. This paper proposes an adaptive, per-block cache update mechanism, which can ensure data consistency of block data in a distributed file system, with low synchronization overhead. Specifically, based on the recent history of read/write requests, the proposed scheme can adaptively select the best-suited consistency update policy for each data block at run time. The experiments on database applications show that our newly proposed mechanism can greatly reduce the overhead resulted by maintaining cache consistency, especially for the workloads having fluctuating read/write ratios. As a consequence, the system performance can be also enhanced
LIAO Jianwei, CAI Zhigang, TRAHAY François, PENG Xiaoning
Block placement in distributed file systems based on block access frequency. IEEE access, june 2018, vol. 6, pp. 38411-38420
URL: https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8400509
abstract
This paper proposes a new data placement policy to allocate data blocks across storage servers of distribute/parallel file systems, for yielding even block access workload distribution. To this end, we first analyze the history of block access sequence of a specific application, and then introduce a k-partition algorithm to divide data blocks into multiple groups, by referring their access frequency. After that, each group has almost same access workloads, we can thus distribute these block groups onto storage servers of distributed file system, to achieve the goal of uniformly assigning data blocks when running the application. In summary, this newly proposed data placement policy can yield not only an even data distribution, but also the block data access balance. The experimental results show that the proposed scheme can greatly reduce I/O time and better improve utilization of storage servers when running the database-relevant applications, compared with the commonly used block data placement strategy, i.e. the round-robin placement policy
LIAO Jianwei, CAI Zhigang, TRAHAY François, JUN Zhou, XIAO Guoqiang
Adaptive process migrations in coupled applications for exchanging data in local file cache. ACM transactions on autonomous and adaptive systems (TAAS), july 2018, vol. 13, n° 2, pp. Article n° 9
abstract
Many problems in science and engineering are usually emulated as a set of mutually interacting models, resulting in a coupled or multiphysics application. These component models show challenges originating from their interdisciplinary nature and from their computational and algorithmic complexities. In general, these models are independently developed and maintained, so that they commonly employ the global file system for exchanging their data in the coupled application. To effectively use the local file cache on the compute node for exchanging the data among the processes of such applications, and consequently boosting I/O performance, this article presents a novel mechanism to migrate a process from one compute node to another node on the basis of block I/O dependency. In this newly proposed mechanism, the block I/O dependency between two involved processes running on the different nodes is profiled as block access similarity by taking advantage of the Cohen's kappa statistic. Then, the process is supposed to be dynamically migrated from its source node to the destination node, on which there is another process having heavy block I/O dependency. As a result, both processes can exchange their data by utilizing the local file cache instead of the global file system to reduce I/O time. The experimental results demonstrate that the I/O performance can be significantly improved, and the time required for executing the application can be resultantly decreased, as expected
RADDAOUI Badran
On the measure of conflicts: an argumentation based framework . Journal of applied non-classical logics, may 2018, vol. 28, n° 2-3, pp. 240-259
abstract
An important issue in the management of knowledge-based systems is the handling of in- consistency. This problem has recently been attracting a lot of attention from Artificial Intelligence community. When inconsistency occurs in a knowledge base, there are mainly two ways to deal with it; we either resolve it or accept inconsistency and cope with it. This paper tackles the problem of evaluating the amount of contradiction in propositional knowledge bases, and provides a new measure of conflict based on deductive argumentation theory. Measuring the degree of conflict of a knowledge base can help us to deal with incon- sistencies. Several semantic- and syntax-based approaches have been proposed separately. Given the pivotal role of argumentation in representing and handling inconsistency, in this paper, we use logical argumentation as a way to compute the inconsistency measure for propositional formulae. We show using the complete argumentation tree that our family of inconsistency measures is able to localise the conflict of a formula following its context and allows us to distinguish between formulae. We extend our measure to quantify the degree of inconsistency of a set of formulae and give a general formulation of the inconsistency using some logical properties. We also provide a general formulation of our method in order to quantify the conflict of the whole knowledge base. Finally, we address the problem of restoring consistency using inconsistency measures
SFAR Hela, BOUZEGHOUB Amel, RADDAOUI Badran
Early anomaly detection in smart home: a causal association rule-based approach. Artificial intelligence in medicine, september 2018, vol. 91, pp. 57-71
abstract
As the world's population grows older, an increasing number of people are facing health issues. For the elderly, living alone can be difficult and dangerous. Consequently, smart homes are becoming increasingly popular. A sensor-rich environment can be exploited for healthcare applications, in particular, anomaly detection (AD). The literature review for this paper showed that few works consider environmental factors to detect anomalies. Instead, the focus is on user activity and checking whether it is abnormal, i.e., does not conform to expected behavior. Furthermore, reducing the number of anomalies using early detection is a major issue in many applications. In this context, anomaly-cause discovery may be helpful in recommending actions that may prevent risk. In this paper, we present a novel approach for detecting the risk of anomalies occurring in the environment regarding user activities. The method relies on anomaly-cause extraction from a given dataset using causal association rules mining. These anomaly causes are utilized afterward for real-time analysis to detect the risk of anomalies using the Markov logic network machine learning method. The detected risk allows the method to recommend suitable actions to perform in order to avoid the occurrence of an actual anomaly. The proposed approach is implemented, tested, and evaluated for each contribution using real data obtained from an intelligent environment platform and real data from a clinical datasets. Experimental results prove our approach to be efficient in terms of recognition rate
ZHOU Zhangbing , ZHAO Deng, HANCKE Gerhard , SHU Lei , SUN Yunchuan
Cache-aware query optimization in multiapplication sharing wireless sensor networks. IEEE transactions on systems, man, and cybernetics. Systems, march 2018, vol. 48, n° 3, pp. 401-417
abstract
Hosting multiple applications in a shared infrastructure of wireless sensor networks is a trend nowadays, and sharing sensory data for answering concurrent applications is a promising and energy-efficient strategy. To address this challenge, this paper proposes an energy-efficient query optimization mechanism for supporting multiple concurrent applications leveraging our two-tier cooperative caching mechanism. Specifically, query requests for concurrent applications are represented as binary strings, which are reduced to a single one for avoiding the reprocessing of shared subquery requests. This reduced query request is answered through our cooperative caching mechanism, where sensory data, which are highly possible to be reused for answering forthcoming query requests, are cached at the sink node (SN). Besides, the gray model GM(1, 1) is adopted for forecasting sensory data units which may be interested mostly by forthcoming query requests. These units of sensory data may be prefetched from the network and cached at the SN. Experimental evaluation shows that this approach can reduce the energy consumption significantly, and improve the network capacity to an extent, especially when the number of concurrent query requests is relatively large
ZHOU Zhangbing , CHENG Zehui, ZHANG Liang-Jie, GAALOUL Walid, NING Ke
Scientific workflow clustering and recommendation leveraging layer hierarchical analysis. IEEE transactions on services computing, january 2018, vol. 11, n° 1, pp. 169-183
abstract
This article proposes an approach for identifying and recommending scientific workflows for reuse and repurposing. Specifically, a scientific work- flow is represented as a layer hierarchy, which specifies hierarchical relations between this workflow, its subworkflows, and activities. Semantic similarity is calculated between layer hierarchies of workflows. A graphskeleton based clustering technique is adopted for grouping layer hierarchies into clusters. Barycenters in each cluster are identified, which refer to core workflows in this cluster, for facilitating cluster identification and workflow ranking and recommendation. Experimental evaluation shows that our technique is efficient and accurate on ranking and recommending appropriate clusters and scientific workflows with respect to specific requirements of scientific experiments
Communication dans une conférence à comité de lecture (23)
ABDELLATIF Safa, BEN HASSINE Mohamed Ali, BEN YAHIA Sadok, BOUZEGHOUB Amel
ARCID: a new approach to deal with imbalanced datasets classification. SOFSEM 2018 : 44th International Conference on Current Trends in Theory and Practice of Computer Science, Cham : Edizioni della Normale, 29 january - 02 february 2018, Krems, Austria, 2018, pp. 569-580, ISBN 978-3-319-73116-2
abstract
Classification is one of the most fundamental and well-known tasks in data mining. Class imbalance is the most challenging issue encountered when performing classification, i.e. when the number of instances belonging to the class of interest (minor class) is much lower than that of other classes (major classes). The class imbalance problem has become more and more marked while applying machine learning algorithms to real-world applications such as medical diagnosis, text classification, fraud detection, etc. Standard classifiers may yield very good results regarding the majority classes. However, this kind of classifiers yields bad results regarding the minority classes since they assume a relatively balanced class distribution and equal misclassification costs. To overcome this problem, we propose, in this paper, a novel associative classification algorithm called Association Rule-based Classification for Imbalanced Datasets (ARCID). This algorithm aims to extract significant knowledge from imbalanced datasets by emphasizing on information extracted from minor classes without drastically impacting the predictive accuracy of the classifier. Experimentations, against five datasets obtained from the UCI repository, have been conducted with reference to four assessment measures. Results show that ARCID outperforms standard algorithms. Furthermore, it is very competitive to Fitcare which is a class imbalance insensitive algorithm
AIT WAKRIME Abderrahim, GIBSON John Paul, RAFFY Jean-Luc
Formalising the requirements of an e-voting software product line using event-B. WETICE 2018: 27th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, Los Alamitos : IEEE Computer Society, 27-29 june 2018, Paris, France, 2018, pp. 78-84, ISBN 978-1-5386-6916-7
[PDF]
abstract
A Software Product Line (SPL) is a tool/method used to generate a family of program/system variants for a specific domain, and to support a more efficient software devel- opment of future products within the same domain. A Feature Model (FM) is a popular graphical/textual representation used in SPL requirements specification; it is used to capture commonality and variability information existing in an SPL as a set of inter- related and configurable features. A concrete model of an SPL instance is obtained by binding the variation information in the FM with a configuration that meets a specific set of feature requirements. Since configuration decisions are taken prior to instantiation, invalid configurations should be detected/avoided before design begins. This paper addresses the problem of the verification of the correctness (validity) of FM instances and FM configuration during requirements modelling. It proposes a requirements model based on Event-B contexts, allowing us to check the correctness of a given configuration, before starting the correct-by-construction design and implementation process, based on refinement.
AIT-AMEUR Yamine, AIT-SADOUNE Idir, CASTERAN Pierre, GIBSON John Paul, HACID Kahina, KHERROUBI Souad, MÉRY Dominique, MOHAND-OUSSAID Linda, SINGH Neeraj, VOISIN Laurent
On the importance of explicit domain modelling in refinement-based modelling design: experiments with Event-B. ABZ 2018: 6th International ABZ Conference on Abstract State Machines, Alloy, B, TLA, VDM and Z, Cham : Springer, 05-08 june 2018, Southampton, United Kingdom, 2018, pp. 425-430, ISBN 978-3-319-91270-7
[PDF]
abstract
Although several authors like P. Zave and M. Jackson, D. Bjorner, A. Van Lamsweerde have drawn the attention of system designers on the necessity to handle domain knowledge, while designing systems, it is still a major concern nowadays. The IMPEX7 project, funded by the French ANR national research agency, addresses the problem of making explicit domain knowledge in formal system developments using refinement and proof based formal methods. It advocates the use and formalisation of ontologies as models for domain knowledge. The Event-B modelling technique has shown its usefulness to support the various developments. In this paper, we briefly describe the approach and the case studies developed in the context of this project
AUSSEL Nicolas, PETETIN Yohan, CHABRIDON Sophie
Improving performances of log mining for anomaly prediction through NLP-based log parsing. MASCOTS 2018: 26th International Symposium on the Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, Los Alamitos : IEEE Computer Society, 25-28 september 2018, Milwaukee, United States, 2018, pp. 237-243, ISBN 978-1-5386-6886-3
abstract
Failure prediction of industrial systems is a promising application domain for data mining approaches and should naturally rely on log messages which are a prime source of data as they are generated by many systems. However, before extracting relevant information of such log messages, another critical step is to parse the logs, that is to say to transform a raw unstructured text from the log messages into a suitable input for data mining. These two problems (log parsing then log mining) are often studied separately while they are directly related in the context of failure prediction ; moreover, few performance benchmarks are publicly available. In this paper, we focus on the impact of log parsing techniques via natural language processing on the performances of log mining on two datasets. The first one is a log of an industrial aeronautical system comprising over 4, 500, 000 messages collected over one year of operation ; the second one is a public benchmark set from an HDFS cluster. On the latter, we show that it is possible to raise the F-score from 96% to 99.2% while using simpler and more robust log parsing techniques that require less parameter tuning provided that they are correctly combined with log mining techniques
BOUDANE Abdelhamid, JABBOUR Saïd, RADDAOUI Badran, SAIS Lakhdar
Efficient SAT-based encodings of conditional cardinality constraints. LPAR-22 2018: 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, 16-21 november 2018, Awassa , Ethiopia, 2018 (document in press)
abstract
In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formula. To avoid combinatorial explosion, the Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, the polarity of the sub-formula Φ is taken into account leading to conditional constraints of the form y → Φ, or Φ → y, where y is a fresh propositional variable. In the case where Φ represents a cardinality constraint, such translation leads to conditional cardinality constraints subject of the present paper. We first show that when all the clauses encoding the cardinality constraint are augmented with an additional new variable, most of the well-known encodings cease to maintain the generalized arc consistency property. Then, we consider some of these encodings and show how they can be extended to recover such important property. An experimental validation is conducted on a SAT-based pattern mining application, where such conditional cardinality constraints is a cornerstone, showing the relevance of our proposed approach
CALDAS Jorge Daniel, LOPES GANCARSKI Alda, RANGEL HENRIQUES Pedro
Online social networks analysis visualization using Socii. WorldCIST 2018 : 6th World Conference on Information Systems and Technologies, Cham : Springer, 27-29 march 2018, Naples, Italy, 2018, vol. 2, pp. 218-228, ISBN 978-3-319-77711-5
abstract
Nowadays we face an age of massive Internet usage. With Online Social Networks (OSN) we practically live this parallel reality where everything we do and everyone we met is exposed and shared through these online "worlds". Today, being able to study and understand how information flows and how relationships are built within these online networks is of paramount importance for various reasons, social, educational, political or economical. That is why social networks analysis has become an important scientific and technological challenge. In this paper, we propose the Socii system for social networks analysis and visualization. Socii aims at helping OSNs users to exploit and understand their own networks through a user friendly interface. The system relies in four main principles, namely simplicity, accessibility, OSNs integration and contextual analysis. Socii's architecture and implementation technological choices are presented, together with its main functionalities
GIBSON John Paul, MÉRY Dominique
Explicit modelling of physical measures: from Event-B to Java. IMPEX 2017: 1st International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development, Electronic Proceedings in Theoretical Computer Science, 13-17 november 2017, Xi’An, China, 2018, vol. 271, pp. 64-79
[PDF]
abstract
The increasing development of cyber-physical systems (CPSs) requires modellers to represent and reason about physical values. This paper addresses two major, inter-related, aspects that arise when modelling physical measures. Firstly, there is often a heterogeneity of representation; for example: speed can be represented in many different units (mph, kph, mps, etc...). Secondly, there is inco- herence in composition; for example: adding a speed to a temperature would provide a meaningless result in the physical world, even though such a purely mathematical operation is meaningful in the abstract. These aspects are problematic when implicit semantics - concerned with measurements - in CPSs are not explicit (enough) in the requirements, design and implementation models. We present an engineering approach for explicitly modelling measurements during all phases of formal system development. We illustrate this by moving from Event-B models to Java implementations, via object oriented design
GIBSON John Paul, GORM LARSEN Peter , PANTEL Marc, FITZGERALD John, WOODCOCK Jim
Cyber-physical systems engineering: an introduction. ISOLA 2018: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Cham : Springer , 05-09 november 2018, Limassol, Cyprus, 2018, pp. 407-410, ISBN 978-3-030-03423-8
[PDF]
abstract
Cyber-Physical Systems (CPSs) [1] connect the real world to software systems through a network of sensors and actuators in which physical and logical components interact in complex ways. There is a diverse range of application domains [2], including health [3], energy [4], transport [5], autonomous vehicles [6] and robotics [7]; and many of these include safety critical requirements [8]. Such systems are, by defi- nition, characterised by both discrete and continuous components. The development and verification processes must, therefore, incorporate and integrate discrete and continuous models. The development of techniques and tools to handle the correct design of CPSs has drawn the attention of many researchers. Continuous mod- elling approaches are usually based on a formal mathematical expression of the problem using dense reals and differential equations to model the behaviour of the studied hybrid system. Then, models are simulated in order to check required properties. Discrete modelling approaches rely on formal methods, based on abstraction, model-checking and theorem prov- ing. There is much ongoing research concerned with how best to combine these approaches in a more coherent and pragmatic fashion, in order to support more rigorous and automated hybrid-design verification. It is also possible to combine different discrete-event and continuous- time models using a technique called co-simulation. This has been sup- ported by different tools and the underlying foundation for this has been analysed. Thus, the track will also look into these areas as well as the industrial usage of this kind of technology
JABBOUR Saïd, MANA Fatima Ezzahra, OULED DLALA Imen, RADDAOUI Badran, SAIS Lakhdar
On maximal frequent itemsets mining with constraints. CP 2018 : 24th International Conference on Principles and Practice of Constraint Programming, Cham : Springer, 27-31 august 2018, Lille, France, 2018, pp. 554-569, ISBN 978-3-319-98333-2
abstract
Recently, a new declarative mining framework based on constraint programming (CP) and propositional satisfiability (SAT) has been designed to deal with several pattern mining tasks. The itemset mining problem has been modeled using constraints whose models cor- respond to the patterns to be mined. In this paper, we propose a new propositional satisfiability based approach for mining maximal frequent itemsets that extends the one proposed in [20]. We show that instead of adding constraints to the initial SAT based itemset mining encoding, the maximal itemsets can be obtained by performing clause learning during search. A major strength of our approach rises in the compactness of the proposed encoding and the efficiency of the SAT-based maximal itemsets enumeration derived using blocked clauses. Experimental results on several datasets, show the feasibility and the efficiency of our approach
JABBOUR Saïd, MHADHBI Nizar, RADDAOUI Badran, SAIS Lakhdar
Pushing the envelope in overlapping communities detection. IDA 2018: 17th international symposium on Intelligent Data Analysis, Cham : Springer, 24-26 october 2018, 'S-Hertogenbosch, Netherlands, 2018, pp. 151-163, ISBN 978-3-030-01767-5
abstract
Discovering the hidden community structure is a fundamental problem in network and graph analysis. Several approaches have been proposed to solve this challenging problem. Among them, detecting overlapping communities in a network is a usual way towards understanding the features of networks. In this paper, we propose a novel approach to identify overlapping communities in large complex networks. It makes an original use of a new community model, called k-clique-star, to discover densely connected structures in social interactions. We show that such model allows to ensure a minimum density on the discovered communities and overcomes some weaknesses of some existing cohesive structures. Experimental results demonstrate the effectiveness and efficiency of our overlapping community model in a variety of real graphs
JABBOUR Saïd, MHADHBI Nizar, RADDAOUI Badran, SAIS Lakhdar
Triangle-driven community detection in large graphs using propositional satisfiability. AINA 2018: 32nd International Conference on Advanced Information Networking and Applications, Los Alamitos : IEEE Computer Society, 16-18 may 2018, Cracow, Poland, 2018, pp. 437-444, ISBN 978-1-5386-2195-0
abstract
Discovering the latent community structure is cru- cial to understanding the features of networks. Several approaches have been proposed to solve this challenging problem using different measures or data structures. Among them, detecting overlapping communities in a network is an usual way towards network structure discovery. It presents nice algorithmic issues, and plays an important role in complex network analysis. In this paper, we propose a new approach to detect overlapping communities in large complex networks. First, we introduce a novel subgraph concept based on triangles to capture the cohesion in social interactions, and propose an efficient approach to discover clusters in networks. Next, we show how the problem of detecting overlapping communities can be expressed as a Partial Max-SAT optimization problem. Our comprehensive experimental evaluation on publicly available real-life networks with ground-truth communities demonstrates the effectiveness and efficiency of our proposed method
JABBOUR Saïd, MHADHBI Nizar, RADDAOUI Badran, SAIS Lakhdar
Detecting highly overlapping community structure by model-based maximal clique expansion. BigData 2018: IEEE international conference on Big Data, Los Alamitos : IEEE Computer Society, 10-13 december 2018, Seattle, United States, 2018 (document in press)
abstract
Community detection, also known as graph clustering, has been extensively studied in the literature. The goal of community detection is to partition vertices in a complex graph into densely-connected components so-called communities. Discovering the hidden community structure is a fundamental problem in network and graph analysis. Several approaches have been proposed to solve this challenging problem. Among them, detecting overlapping communities in a network is an usual way towards understanding the features of networks. In this paper, we propose an efficient overlapping community detection method using a seed set expansion approach. In particular, we make an original use of a particular concept of graph theory, called chordal graph, to discover densely connected structures in social interactions based on maximal cliques. Indeed, a chordal graph possesses a number of interesting and useful properties that can help us to efficiently recover all maximal cliques of a given graph. Then, we develop new seeding strategies based on different fitness functions for discovering meaningful communities. Experimental results demonstrate the effectiveness and the efficiency of our overlapping community model in a variety of real graphs
JARRAYA Amina, BOUZEGHOUB Amel, BORGI Amel, AROUR Khedija
Distributed collaborative reasoning for HAR in smart homes. AAMAS 2018 : 17th International Conference on Autonomous Agents and MultiAgent Systems, Richland : International Foundation for Autonomous Agents and Multiagent Systems, 10-15 july 2018, Stockholm, Sweden, 2018, pp. 1971-1973
URL: http://ifaamas.org/Proceedings/aamas2018/pdfs/p1971.pdf
abstract
Distributed Human Activity Recognition (D-HAR) is an active research issue for pervasive computing that aims to identify human activities in smart homes. This paper proposes a fully distributed multi-agent reasoning approach where agents, with diverse classifiers, observe sensor data, make local predictions and collaborate to identify current activities. Experimental tests on Aruba dataset indicate an enhancement in terms of accuracy and F-measure metrics compared either to a centralized approach or a distributed approach from the literature
MAMMAR Amel, FRAPPIER Marc, TUENO Steve , LALEAU Régine
An Event-B model of the hybrid ERTMS/ETCS level 3 standard. ABZ 2018: 6th International ABZ Conference on Abstract State Machines, Alloy, B, TLA, VDM and Z, Cham : Springer, 05-08 june 2018, Southampton, United Kingdom, 2018, pp. 353-366, ISBN 978-3-319-91270-7
abstract
This paper presents an Event-B model of the ABZ2018 case study on the European Rail Trac Management System (ERTMS) standard. The case study focusses on the management of xed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not tted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four renements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved
MOHAMED Mohamed, ANYA Obinna, TAKASHI Sakairi, TATA Samir, NAGAPRAMOD Mandagere, HEIKO Ludwig
The rSLA framework : monitoring and enforcement of service level agreements for cloud services. SCC 2016 : 13th International Conference on Services Computing, Los Alamitos : IEEE Computer Society, 27 june - 02 july 2016, San Francisco, United States, 2018, pp. 625-632, ISBN 978-1-5090-2628-9
abstract
Managing service quality in heterogeneous Cloud environments is complex: different Cloud providers expose different management interfaces. To manage Service Level Agreements (SLAs) in this context, we have developed the rSLA framework that enables fast setup of SLA monitoring in dynamic and heterogeneous Cloud environments. The rSLA framework is made up of three main components: the rSLA language to formally represent SLAs, the rSLA Service, which interprets the SLAs and implements the behavior specified in them, and a set of Xlets - lightweight, dynamically bound adapters to monitoring and controlling interfaces. In this paper, we present the rSLA framework, and describe how it enables the monitoring and enforcement of service level agreements for heterogeneous Cloud services
OUDART David, CANTENOT Jérôme, BOULANGER Frédéric, CHABRIDON Sophie
Démarche de conception d'un réseau électrique intelligent et de son système d'information par cosimulation. CIEL 2018 : 7ème Conférence en IngénieriE du Logiciel , France : CNRS, 14-15 juin 2018, Grenoble, France, 2018, pp. 9-1-9-5
URL: http://gdr-gpl.cnrs.fr/node/329
[PDF]
abstract
Les réseaux électriques intelligents, dits Smart Grids, sont la prochaine génération de réseaux de distribution d'électricité, qui s'appuient sur les technologies de l'information pour soutenir l'intégration des sources de production d'énergie décentralisées et intermittentes telles que les parcs éoliens et les centrales photovoltaı̈ques. Ils dépendent de plusieurs domaines comme ceux de la physique et du génie électrique, du logiciel et des réseaux de télécommunications. La conception de réseaux électriques intelligents est donc complexe en raison des différents domaines techniques et outils de modélisation en jeu. Dans cet article, nous présentons une approche de conception s'appuyant sur l'ingénierie dirigée par les modèles, les modèles exécutables et la cosimulation FMI. Cette approche est illustrée sur le cas d'utilisation de la conception d'un réseau électrique insulaire, et permet d'étudier l'effet des décisions de production d'électricité
OULED DLALA Imen, JABBOUR Saïd, RADDAOUI Badran, SAIS Lakhdar
A parallel SAT-based framework for closed frequent itemsets mining. CP 2018: 24th International Conference on Principles and Practice of Constraint Programming, Cham : Springer, 27-31 august 2018, Lille, France, 2018, pp. 570-587, ISBN 978-3-319-98333-2
abstract
Constraint programming (CP) and propositional satisfiabil- ity (SAT) based framework for modeling and solving pattern mining tasks has gained a considerable audience in recent years. However, this nice declarative and generic framework encounters a scaling problem. The huge size of constraints networks/propositional formulas encoding large datasets is identified as the main bottleneck of most existing ap- proaches. In this paper, we propose a parallel SAT based framework for itemset mining problem to push forward the solving efficiency. The pro- posed approach is based on a divide-and-conquer paradigm, where the transaction database is partitioned using item-based guiding paths. Such decomposition allows us to derive smaller and independent Boolean for- mulas that can be solved in parallel. The performance and scalability of the proposed algorithm are evaluated through extensive experiments on several datasets. We demonstrate that our partition-based parallel SAT approach outperforms other CP approaches even in the sequential case, while significantly reducing the performances gap with specialized approaches
RAKOCZY Monika, BOUZEGHOUB Amel, LOPES GANCARSKI Alda, WEGRZYN-WOLSKA Katarzyna
Influence in time-dependent citation networks. RCIS 2018: 12th International Conference on Research Challenges in Information Science, Los Alamitos : IEEE Computer Society, 29-31 may 2018, Nantes, France, 2018, pp. 1-11, ISBN 978-1-5386-6517-6
abstract
In this paper, we present a running influence model for evaluating the pairwise impact between communities in citation networks and define the time limitations of the model. The model improves a recent one from the literature. To compare and contrast different communities influence, we present a metric for estimating the overall running influence value of particular community. We also study the problem of the time dependency of the influence within citation networks. To conduct the community influence analysis, we perform the experiments using a real-world database. The results are compared to both real-world ranking and the state-of-the-art method. They show the adequacy of the proposed metrics and model of running influence. We also demonstrate the importance of proposed differentiation within calculation and interpretation of the influence in time-dependent citation networks
SUTRA Pierre, MARLIER Patrick, SCHIAVONI Valerio, TRAHAY François
Boosting transactional memory with stricter serializability. COORDINATION 2018: 20th International Conference on Coordination Models and Languages, Cham : Springer, 18-21 june 2018, Madrid, Spain, 2018, pp. 231-251, ISBN 978-3-319-92407-6
abstract
Transactional memory (TM) guarantees that a sequence of operations encapsulated into a transaction is atomic. This simple yet powerful paradigm is a promising direction for writing concurrent applications. Recent TM designs employ a time-based mechanism to leverage the performance advantage of invisible reads. With the advent of many-core architectures and non-uniform memory (NUMA) architectures, this technique is however hitting the synchronization wall of the cache coherency protocol. To address this limitation, we propose a novel and flexible approach based on a new consistency criteria named stricter serializability ( SSER+ ). Workloads executed under SSER+ are opaque when the object graph forms a tree and transactions traverse it top-down. We present a matching algorithm that supports invisible reads, lazy snapshots, and that can trade synchronization for more parallelism. Several empirical results against a well-established TM design demonstrate the benefits of our solution
TRAHAY François, SELVA Manuel, MOREL Lionel, MARQUET Kevin
NumaMMA: Numa MeMory Analyzer. ICPP 2018: 47th International Conference on Parallel Processing, New York : ACM, 13-16 august 2018, Eugene, United States, 2018, pp. 19-1-19-10, ISBN 978-1-4503-6510-9
[PDF]
abstract
Non Uniform Memory Access (NUMA) architectures are nowadays common for running High-Performance Computing (HPC) appli- cations. In such architectures, several distinct physical memories are assembled to create a single shared memory. Nevertheless, be- cause there are several physical memories, access times to these memories are not uniform depending on the location of the core performing the memory request and on the location of the target memory. Hence, threads and data placement are crucial to effi- ciently exploit such architectures. To help in taking decision about this placement, profiling tools are needed. In this work, we propose NUMA MeMory Analyzer (NumaMMA), a new profiling tool for understanding the memory access patterns of HPC applications. NumaMMA combines efficient collection of memory traces using hardware mechanisms with original visualization means allowing to see how memory access patterns evolve over time. The informa- tion reported by NumaMMA allows to understand the nature of these access patterns inside each object allocated by the application. We show how NumaMMA can help understanding the memory patterns of several HPC applications in order to optimize them and get speedups up to 28% over the standard non optimized version
TUENO Steve , FRAPPIER Marc, LALEAU Régine, MAMMAR Amel, LEUSCHEL Michael
Formalisation of SysML/KAOS goal assignments with B system component decompositions. IFM 2018: 14th International Conference on Integrated Formal Methods, Cham : Springer, 05-07 september 2018, Maynooth, Ireland, 2018, pp. 377-397, ISBN 978-3-319-98937-2
abstract
The use of formal methods for verification and validation of critical and complex systems is important, but can be extremely tedious without modularisation mechanisms. SysML/KAOS is a requirements engineering method. It includes a goal modeling language to model requirements from stakeholder's needs. It also contains a domain modeling language for the representation of system application domain using ontologies. Translation rules have been defined to automatically map SysML/KAOS models into B System specifications. Moreover, since the systems we are interested in naturally break down into subsystems (enabling the distribution of work between several agents: hardware, software and human), SysML/KAOS goal models allow the capture of assignments of requirements to agents responsible of their achievement. Each agent is associated with a subsystem. The contribution of this paper is an approach to ensure that a requirement assigned to a subsystem is well achieved by the subsystem. A particular emphasis is placed on ensuring that system invariants persist in subsystems specifications
TUENO Steve , MAMMAR Amel, LALEAU Régine, FRAPPIER Marc
Event-B expression and verification of translation rules between SysML/KAOS domain models and B system specifications. ABZ 2018: 6th International ABZ Conference on Abstract State Machines, Alloy, B, TLA, VDM and Z, Cham : Springer, 05-08 june 2018, Southampton, United Kingdom, 2018, pp. 55-70, ISBN 978-3-319-91270-7
abstract
This paper is about the extension of the SysML/KAOS requirements engineering method with domain models expressed as ontologies. More precisely, it concerns the translation of these ontologies into B System for system construction. The contributions of this paper are twofold. The first one is a formal semantics for the ontology modeling language. The second one is the formal definition of translation rules between ontologies and B system specifications in order to provide the structural part of the formal specification. These translation rules are modeled in Event-B. Their consistency and completeness are proved using Rodin. We show that they are structure preserving (two related elements within the source model remain related within the target model), by proving various isomorphisms between the ontology and the B System specification
TUENO Steve , FRAPPIER Marc, LALEAU Régine, MAMMAR Amel
Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. ABZ 2018: 6th International ABZ Conference on Abstract State Machines, Alloy, B, TLA, VDM and Z, Cham : Springer, 05-08 june 2018, Southampton, United Kingdom, 2018, pp. 262-276, ISBN 978-3-319-91270-7
abstract
This paper presents a specification of the hybrid ERTMS/ ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover
