Université Constantine 2
Abdelhamid Mehri University Constantine2 Scholarlyworks RepositoryNot a member yet
128 research outputs found
Sort by
A Strategy-Based Formal Approach for Fog Systems Analysis
No full textThis work is licensed under a Creative Commons Attribution 4.0 International License.Fog systems are a new emergent technology having a wide range of architectures and pronounced needs making their design complex. Consequently, the design of fog systems is crucial, including service portability and interoperability between the various elements of a system being the most essential aspects of fog computing. This article presents a fog system cross-layer architecture as a first step of such a design to provide a graphical and conceptual description. Then, a BiAgents* (Bigraphical Agents) formal model is defined to provide a rigorous description of physical, virtual, and behavioural aspects of Fog systems. Besides, this formalisation is implemented and executed under a Maude strategy system. The proposed approach is illustrated through a case study: an airport terminal Luggage Inspection System (LIS) while checking the correctness of its relevant properties: the portability of data and their interoperability. The integration of the Maude strategies in the rewriting of Fog system states made it possible to guide the execution of the model and its analysis.14
A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems
No full textThis work is licensed under a Creative Commons Attribution 4.0 International License.This paper proposes an approach integrating UML 2.0 Activity Diagrams (UML2-AD) and Communicating Sequential Process (CSP) for modeling and verication of software systems. A UML2-AD is used for modeling a software system while CSP is used for verication purposes. The proposed approach consists of another way of transforming UML2-AD models to Communicating Sequential Process (CSP) models. It focuses also on checking the correctness of some properties of the transformation itself. These properties are specified using Linear Temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on Model Driven Engineering (MDE). The meta-modelling is realized using AToMPM tool while the model transformation and the correctness of its properties are realized using GROOVE tool. Finally, we illustrated this approach through a case study.220
Internet of Things Meet Internet of Threats: New Concern Cyber Security Issues of Critical Cyber Infrastructure
No full textAs a new area of technology, the Internet of Things (IoT) is a flagship and promising paradigm for innovating society. However, IoT-based critical infrastructures are an appealing target for cybercriminals. Such distinctive infrastructures are increasingly sensitive to cyber vulnerabilities and subject to many cyberattacks. Thus, protecting these infrastructures is a significant issue for organizations and nations. In this context, raising the cybersecurity posture of critical cyber infrastructures is an extremely urgent international issue. In addition, with the rapid development of adversarial techniques, current cyber threats have become more sophisticated, complicated, advanced and persistent. Thus, given these factors, prior to implementing efficient and resilient cybersecurity countermeasures, identification and in-depth mapping of cyber threats is an important step that is generally overlooked. Therefore, to solve cybersecurity challenges, this study presents a critical analysis of the most recent cybersecurity issues for IoT-based critical infrastructures. We then discuss potential cyber threats and cyber vulnerabilities and the main exploitation strategies adopted by cybercriminals. Further, we provide a taxonomy of cyberattacks that may affect critical cyber infrastructures. Finally, we present security requirements and some realistic recommendations to enhance cybersecurity solutions.111
Formal verification of the extension of iStar to support Big data projects
No full textIdentifying all the right requirements is indispensable for the success of any system. These requirements need to be engineered with precision in the early phases. Principally, late corrections costs are estimated to be more than 200 times as much as corrections during requirements engineering (RE). Especially Big data area, it becomes more and more crucial due to its importance and characteristics. In fact, and after literature analyzing, we note that currents RE methods do not support the elicitation of Big data projects requirements. In this study, we propose the BiStar novel method as extension of iStar to under- take some Big data characteristics such as (volume, variety ...etc). As a first step, we identify some missing concepts that currents requirements engineering methods do not support. Next, BiStar, an extension of iStar is developed to take into account Big data specifics characteristics while dealing with require- ments. In order to ensure the integrity property of BiStar, formal proofs were made, we perform a bigraph based description on iStar and BiStar. Finally, an application is conducted on iStar and BiStar for the same illustrative scenario. The BiStar shows important results to be more suitable for eliciting Big data projects requirements.220
Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
No full textThe profile UML MARTE offers a general modeling framework for designing and analyzing real-time and embedded systems. Temporal aspects are critical criteria that should be taken into account during the design process. So, formal methods may be used to ensure the functional correctness of such systems. For this purpose, this paper defines an operational method for translating UML sequence diagrams annotated with MARTE stereotypes to time Petri nets with action duration specifications. The semantics of these specifications are defined in terms of duration action timed automata. This allows formal verification by means of several model checker tools like UPPAAL.390
A takeover time-driven adaptive evolutionary algorithm for mobile user tracking in pre-5G cellular networks
No full textCellular networks are one of today’s most popular means of communication. This fact has made the mobile phone industry subject to a huge scientific and economic competition, where the quality of service is key. Such a quality is measured on the basis of reliability, speed and accuracy when delivering a service to a user no matter his location or behaviour are. This fact has placed the users’ tracking process among the most difficult and determining issues in cellular network design. In this paper, we present an adaptive bi-phased evolutionary algorithm based on the takeover time to solve this problem. The proposal is thoroughly assessed by tackling twenty-five real-world instances of different sizes. Twenty-eight of the state-of-the-art techniques devised to address the users’ mobility problem have been taken as the comparison basis, and several statistical tests have been also conducted. Experiments have demonstrated that our solver outperforms most of the top-ranked algorithms
The role of university governance in harmonizing higher education outputs with labor market requirements- case study of some Arab and European countries
No full textتهدف هذه الدراسة إلى إدراك الدور الذي تؤديه حوكمة الجامعة في مواءمة خريجي التعليم العالي لمتطلبات سوق العمل، والتي تم التطرق فيها للأدبيات النظرية للتعريف بمحاور الدراسة المتمثلة في الحوكمة بالجامعة، متطلبات سوق العمل، وفي الجزء التطبيقي تم عرض نتائج المسح الإحصائي لبعض الجامعات العربية ومقارنتها مع أخرى أوروبية من حيث وضعية الخريجين في سوق العمل وانعكاس تطبيق مبادئ الحوكمة على مؤهلاتهم ومهاراتهم المهنية. وقد أشارت النتائج إلى عدم تطبيق الجامعات العربية محل الدراسة لمبادئ حوكمة الجامعات التي تخدم مخرجات التعليم العالي وانعكاس ذلك على تدني معدلات توظيفهم بعد التخرج مقارنة بالجامعات الأوروبية التي يتميز خريجوها بمعدل توظيف مرتفع في سوق العمل .The aim of the study is to apprehend the role of the university governance in harmonizing higher education outputs with the labor market requirements. We have introduced in the literature part the study axes: the university governance and the market requirements, whereas in the empirical part, we have presented the results of the statistical survey of some Arabic universities, comparing them to other European universities in terms of graduates’ status in labor market and the reflection of the applied principles of governance on their qualifications and professional skills. Results showed that Arab universities did not apply the university governance principles that serve the outputs of higher education, which is reflected in the employment low rates after graduation compared to those of the European universities, where their graduates are distinguished with a high rate of employment by the labor market.0801183
SLA-Driven modeling and verifying cloud systems: A Bigraphical reactive systems-based approach
No full textWe propose a formal approach based on Bigraphical Reactive Systems (BRSs) and model checking techniques for modeling and verifying the interaction behaviours of SLA-based cloud computing systems. In the first phase of this approach, we address the modeling of the static structure and the dynamic behavior of cloud systems using BRSs. We show how bigraphs enable the description of the different cloud entities, including cloud actors, cloud services, Service Level Agreements (SLAs), the diversity of their properties, and the complex interactions and dependencies among them. Furthermore, we propose a four-stages SLA lifecycle, and define a set of bigraphical reaction rules to abstract these stages and model the dynamic nature of the cloud. The second phase of this approach verifies that the behavior of services and cloud actors will cope with the agreed SLA terms during the lifecycle of the SLA. We map the proposed bigraphical models into SMV descriptions. Then, we express the interaction behaviors as a set of liveness and safety properties using Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) formulas, and we use the NuSMV model checker to verify them. Finally, we define a case study on which we illustrate the application of our proposed approach.7
Models@Runtime: The Development and Re-Configuration Management of Python Applications Using Formal Methods
No full textThis work is licensed under a Creative Commons Attribution 4.0 International License.Models@runtime (models at runtime) are based on computation reflection. Runtimemodels can be regarded as a reflexive layer causally connected with the underlying system. Hence,every change in the runtime model involves a change in the reflected system, and vice versa. Tothe best of our knowledge, there are no runtime models for Python applications. Therefore, wepropose a formal approach based on Petri Nets (PNs) to model, develop, and reconfigure Pythonapplications at runtime. This framework is supported by a tool whose architecture consists of twomodules connecting both the model and its execution. The proposed framework considers executionexceptions and allows users to monitor Python expressions at runtime. Additionally, the applicationbehavior can be reconfigured by applying Graph Rewriting Rules (GRRs). A case study usingService-Level Agreement (SLA) violations is presented to illustrate our approach.112
Plagiarism Detection: A focus on the Intrinsic Approach and the Evaluation in the Arabic Language
No full textWith the advent of the Internet and the widespread use of digital documents, access to information from the four corners of the globe has become easier and easier. This was accompanied by the copy-paste phenomenon that curtailed the appropriation of others’ work (i.e., plagiarism) to a few clicks. Since the ‘70s of the last century, researchers have begun developing software to automatically detect textual plagiarism. Still, as the techniques of these programs evolve, the plagiarists develop their tactics to escape them. Therefore, the plagiarism detection tools that have the potential to resist are the ones that are able to fight against this misconduct in different ways. Moreover, in the wake of globalisation, these tools should be able also to handle documents in multiple languages. Thus, given the perpetuation of this problem, the acquisition of the latest plagiarism detection technologies has become like an arms race for a never-ending battle
This thesis deals with two major topics: plagiarism detection in Arabic documents, and plagiarism detection based on the writing style changes in the suspicious document, which is called intrinsic plagiarism detection. This approach is an alternative to the text-matching approach, notably, in the absence of the plagiarism source. Our key contributions in these two areas lie first, in the development of Arabic corpora to allow for the evaluation of plagiarism detection software on this language and, second, in the development of a language-independent intrinsic plagiarism detection method that exploits the character n-grams in a machine learning approach while avoiding the curse of dimensionality. Hence, our third key contribution is an investigation on which character n-grams, in terms of their frequency and length, are the best to detect plagiarism intrinsically. We carried out our experiments on standardised English corpora and also on the developed Arabic corpora using the method we developed and one of the most prominent intrinsic plagiarism detection methods. The findings of our analysis can be exploited by the future intrinsic plagiarism detection methods that use character n-grams. In addition to the above-mentioned technical contributions, we provide the reader with comprehensive and critical surveys of the literature of Arabic plagiarism detection and intrinsic plagiarism detection, which were lacking in both topics