Université Constantine 2
Abdelhamid Mehri University Constantine2 Scholarlyworks RepositoryNot a member yet
128 research outputs found
Sort by
Une approche basée sur l'ingénierie dirigée par les modèles pour la vérification des descriptions AADL
No full textIn this work, we propose an approach for the verification of the AADL (Architecture and Analysis Design Language) description. This approach is based in Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism; we define a transformation process in two steps : the first is aModel2Model transformation which takes an AADLModel and produces the corresponding timed automata model. The second transformation is a Model2Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. The goal of this effort is to insure some properties of AADL models using the Uppaal model checker. A case study has been developed to show the feasibility and validity of the proposed approach.Dans ce travail, nous proposons une approche pour la vérification des descriptions AADL (Architecture and Analysis Design Language). Cette approche est basée sur l’ingénierie dirigée par les modèles (IDM) et assistée par un ensemble d’outils. En effet, nous proposons un méta-modèle source pour AADL et un métamodèle cible pour le formalisme des automates temporisés. Puis, nous définissons un processus de transformation en deux étapes ; la première est une transformation de type Model2Model qui prend un modèle AADL en entrée et produit le modèle d’automates temporisés correspondant en sortie. La deuxième étape est une transformation de type Model2Text qui prend le modèle généré dans la première étape et le transforme en texte dans le code “ta-format”. Ce code est une représentation textuelle interne du model-checker UPPAAL. L’objectif de cette initiative est d’assurer certaines propriétés des modèles AADL comme l’absence de l’interblocage, la sûreté et la vivacité. Une étude de cas a été développé pour démontrer la faisabilité et la validité de l’approche proposée
Effective Bridging Between Ecore and Coq: Case of a Type-Checker with Proof-Carrying Code
No full textThe work presented in this paper lies in the context of implementing supporting tools for a domain-specific language named SosADL, targeted at the description and analysis of architecture for systems of systems. While the language has formal definition rooted in the Cc-pi calculus, we have adopted the Eclipse ecosystem, including EMF, Ecore and Xtext for the convenience they provide in implementation tasks. Proof-carrying code is a well-known approach to ensure such an implementation involving non-formal technologies conforms to its formal definition, by making the implementation generate proof in addition to usual output artifacts. In this paper, we therefore investigate for an infrastructure that eases the development of proof-carrying code for an Eclipse/EMF/Ecore/Xtext-based tool in relation with the Coq proof assistant. At the core of our approach, we combine an automatic transformation of a metamodel into a set of inductive types, in conjunction with a second transformation of model elements into terms. The first one, reused from our previous work, provides necessary abstract syntax definitions such that the formal definition of the language can be mechanized using Coq. The second transformation is part of the proof generator.6425927
Logic Verification of Real Time Systems in the Context of the Maximality Semantics
No full textThe verification by model checking has been widely studied for the timed automata model. This technique is used for automatically verifying correctness properties of finite-state systems based on interleaving semantics. Therefore, the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). The state space of transitions system associated to a durational actions timed automata model is infinite. To verify this model, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics-based verification provides new class of properties related to simultaneous progress of actions at different states. A method that is based on another abstraction of the state space, uses a symbolic representation called zone. We have designed a new zone graph under the maximality semantics, named Maximality-based Zone Graph (MZG), for describing symbolic execution of daTA. An algorithm based on the symbolic and an on-the-y forwards reachability analysis algorithm for durational actions timed automata is proposed. We use Difference Bounded Matrices (DBM), which are one of the most effective data structures for representing zones.La vérification par model checking a été largement étudiée pour le modèle des automates temporisés. C’est une technique de validation pour vérifier automatiquement la correction des propriétés des systèmes états finis, qui sont basées sur la sémantique d’entrelacement, car les actions sont supposées instantanées. Pour échapper l’hypothèse d’atomicité temporelle et structurelle des actions, nous utilisons le modèle des automates temporisés avec durées d’actions (daTA). Ce modèle est basé sur la sémantique de maximalité. Les propriétés vérifier sont exprimées, en utilisant la logique temporelle arborescente temporisée (TCTL). L’espace d’état du système de transitions associé à un automate temporisé avec durées d’actions, est infini. Pour vérifier ce modèle, le graphe des régions basé sur la maximalité (MRG) est déni et une adaptation de l’algorithme de model checking est proposée. L’utilisation de la vérification basée sur la sémantique de maximalité fournit une nouvelle classe de propriétés liées au progrès simultané des actions dans les différents états. Une méthode qui est basée sur une autre abstraction de l’espace d’état, utilise une représentation symbolique appelée zone. Nous avons connu un nouveau graphe des zones sous la sémantique de maximalité, nommé graphe des zones basé sur la maximalité (MZG), pour décrire l’exécution symbolique du daTA. Un algorithme d’analyse d’accessibilité en avant la volée, basé sur la représentation symbolique, pour les automates temporisés avec durées d’actions est proposé. Nous utilisons une structure de données permettant d’implémenter facilement les zones, en l’occurrence les matrices différences bornées (DBM)
استخدام الرسائل والأطروحات الإلكترونية من طرف طلبة ما قبل التدرج لأغراض البحث: دراسة استطلاعية بمعهد علم المكتبات والتوثيق بجامعة قسنطينة 2 - الجزائر
No full textيشهد العصر الحالي تزايدا مطردا في نمو المعلومات وتنوع أشكالها، مما شكل ضغطا على المكتبات نتيجة التغيرات الحالية والتوجه العالمي في بيئة المعلومات الحديثة إلى تبني سياسات لإنتاج المعرفة الأكاديمية ونشرها في أشكال رقمية وإتاحتها للمجتمع الباحثين والدارسين دون قيود في مشاريع المستودعات الرقمية الأكاديمية من أجل تسهيل الاستفادة منها وتوسيع استخدامها والانتفاع بها لأغراض البحث وتحقيق التنمية المستدامة في مجالات النشاط الفكري الإنساني، وهذا لا يتحقق إلا بتبني الوصول الحر إلى المعلومات العلمية حتى تستفيد منها كل الجهات الفاعلة في المحيط الأكاديمي، فمن هذا المنطلق نشأت المستودعات الرقمية المؤسسية لتخطي القيود والعقبات التي تحول دون الوصول إلى المعرفة الأكاديمية من خلال المنشورات في شكلها التقليدي. وتهدف هذه الدراسة إلى تسليط الضوء على واقع استخدام طلبة ما قبل التدرج للرسائل والأطروحات الجامعية الإلكترونية التي توفرها لهم المكتبة لأغراض البحث العلمي، ونماذج الإتاحة المتوفرة لهذا النوع من الأدبيات الرمادية، كما تهدف الدراسة إلى التعرف على مدى فاعلية تلك المصادر في دعم وتعزيز تكوينهم الأكاديمي.28330
The role of MOOC courses in improving the students learning An empirical study at the school of Information and Communication Technologies - the University of Constantine 2-
No full textيهدف هذا البحث إلى دراسة نوع جديد من التعليم عن بعد، عرف باسم موك MOOC، يتميز بانه مفتوح للجميع بدون استثناء، يعتمد على الأنترنت كوسيلة للتواصل بين المعلم والمتعلمين والأهم في كل هذا أنه يقدم من طرف جامعات ومدارس لها سمعة عالمية، وفي كثير من الأحيان بالمجان. من هنا جاءت اشكاليتنا لتحاول معرفة الدور الذي تلعبه دروس الموك "MOOC" في تحسين تكوين الإعلام الآلي لطلبة الجامعة. وكان اختيارنا لطلبة كلية تكنولوجيا الإعلام والاتصال بجامعة قسنطينة 2 باعتبارهم في لقاء مستمر بالأنترنت والتطبيقات التي يوفرها. فتكون لدراستنا نتائج يمكن قياسها من خلال استعمال استمارة استبيان، وزعت على 200 طالب. وكشفت النتائج أن الكثير من الطلبة يجهلون وجود هذه الدروس، والقليل من عرفها وأخذ منها دروس يجدها مفيدة لفهم دروس المنهاج الأكاديمي المتبع في الجامعة.The research aims to answer the following question: what is the of MOOC courses in improving the students learning in computer's sciences? Our choice of the students, from the school of Information and Communication Technologies at the University of Constantine2, is based on their constant use of Internet and the applications that it provides. We have distributed 200 questionnaires, and the results have revealed that many students ignore the existence of these courses where just few of them took some lessons that were found to be useful to understand the academic curriculum courses, established by the university.5
rd-TA and daTA-R : A relative timed models for heterogeneous real time systems
No full textLa vérification des systèmes temps-réel nécessite la proposition d’approches formelles qui permettent la construction des outils de vérification. Dans ce travail, nous adressons la question de l’accessibilité sur des variantes des automates temporisés (TA) dans lesquelles les horloges progressent selon des fréquences relatives. Nous adressons aussi la question de la satisfaction temporelle dans les systèmes multi-agents coordonnés tels que les agents peuvent se comporter en vraie concurrence et peuvent avoir des rythmes relatifs. Dans ce contexte, nous montrons que le problème de la satisfaction peut se réduire à une question d’accessibilité sur un graphe de régions. Nous introduisons les TA dynamiques avec temps relatif (rd-TA) pour pouvoir créer de nouveaux processus hétérogènes. Dans ce modèle, un système temporisé distribué est un ensemble de rd-TA. Chaque rd-TA est caractérisé par un ensemble d'horloges locales qui évoluent selon une fréquence relative par rapport à celles des horloges des autres composants. La contribution principale est la considération du paramètre qui permet de construire une abstraction de régions pour évaluer et prouver la décidabilité. Nous introduisons aussi des règles de dérivation afin de produire, à partir d’une spécification D-LOTOS, un TA étendu avec des durées d’actions et des vitesses relatives du temps (daTA-R)
استخدام مصادر المعلومات الإلكتر ونية من طرف طلبة الدراسات العليا دراسة تحليلية لرسائل الدكتوراه بمعهد علم المكتبات والتوثيق بجامعة عبد الحميد مهري – قسنطينة 2
No full textWe aim through this exploratory study to identify and know the actual orientations of university researchers in the use of electronic information sources when preparing and accomplishing their scientific research. To reach this goal, we analyze reference citations of doctoral theses in both specialties “Libraries and Archives”, from 2010 to 2016, at the Institute of Library science and Documentation, at the university Constantine 2- Abdelhamid Mehri. We try to see how they benefit from the different types of electronic information sources either through free access or across different databases accessible via the national portal for electronic documentation “SNDL”, in Algerian academic institutions.نسعى في هذه الدراسة إلى تحديد ومعرفة التوجهات الحقيقية للباحثين الجامعيين في استخدام مصادر المعلومات الإلكترونية في إنجاز وإعداد أبحاثهم العلمية، من خلال تحليل الاستشهادات المرجعية لرسائل الدكتوراه في تخصص المكتبات و الأرشيف من سنة 2010إلى سنة 2016بمعهد علم المكتبات والتوثيق بجامعة عبد الحميد مهري- قسنطينة- ،-2ومن ثم معرفة مدى استفادتهم من مصادر المعلومات الإلكترونية وأنواعها المختلفة، سواء كان عن طريق الوصول الحر أو من خلال مختلف قواعد المعلومات المتاحة عبر البوابة الوطنية للتوثيق الإلكتروني SNDL47355
Distributed construction of state spaces for an efficient verification of untimed systems
No full textDe nos jours, les applications basées sur les graphes sont largement répandues, en particulier avec la croissance des nouvelles technologies, notamment les applications mobiles, Le World Wide Web, les réseaux sociaux et l’internet des objets. Les applications mobiles sont des exemples où les graphes deviennent dynamiques et de plus en plus larges. Les graphes ne sont pas seulement limités à Internet, le Model checking est un autre exemple important. En effet, le model checking est une technique de vérification automatique des systèmes complexes qui nécessite un graphe modélisant ces systèmes comme une entrée pour fonctionner. Cependant, la taille de ce graphe d’entrée a tendance à être très large en fonction de la complexité du système, ce qui entraîne le problème de l’explosion combinatoire d’espace d’états. Ainsi, dans le cas des systèmes très complexes, le graphe devient difficile à générer et à stocker sur une seule machine en raison de la limitation de capacité matérielle. Les travaux présentés ici proposent deux types de solutions pour traiter plus efficacement des espaces d’états de plus large taille. La première s’appuie sur des ressources parallèles avec des techniques basées sur des algorithmes génétiques et la deuxième traite plus efficacement des diagrammes de décision binaires, en les adaptant au problème de la distribution de l’espace d’états.Nowadays, the application of graphs is widely spread especially with the growth of new technologies. World wide web and social networks are examples of such applications where graphs are becoming dynamic and going larger and larger. Large graphs are not only limited to internet, model checking is another important example likewise. Indeed, the model checking is an automatic technique used to check systems. This technique requires a graph modeling the system as an entry to operate on. However, the size of this entry graph has a tendency to be huge according to the system complexity which results the problem of state space explosion. In fact, in the case of very complex systems, the graph becomes hard to be generated and stored on the same machine because of hardware capacity limitation. The work presented here offer two types of solutions to deal effectively with large state spaces. The first relies on resources parallel cluster computing with techniques based on genetic algorithms. The second proposed deal more effectively with binary decision diagrams by adapting them to the problem of state space distribution
Congestion control techniques in VANETs: A survey
No full textDuring these last years, Intelligent Transport Systems (ITS) have experienced a great growth in both areas: academic and industrial. ITS which aim to increase safety and comfort for users' transport, are essentially governed by Vehicular Ad hoc Networks: VANETs. In such networks, nodes represent smart vehicles that can communicate either between themselves to exchange traffic information or with roadside infrastructure to disseminate or request useful information. Therefore, the congestion control remains one of the most challenging problems of these networks. This paper surveys congestion control techniques, which are divided into three categories: Rate adaptation, Media access control (MAC) and trajectory based schemes. For each technique we give its principle, its merits and its limits. A comparative study with respect to some relevant metrics is given as well