28 research outputs found
SPÉCIFICATION ET VÉRIFICATION DES SYSTÈMES EMBARQUÉS TEMPS RÉEL EN UTILISANT LA LOGIQUE DE RÉÉCRITURE
No full textLes systèmes embarqués temps réel doivent être correctement validés et vérifiés avant de les
fabriquer et déployer afin d'augmenter leurs fiabilités et de réduire leurs coûts de maintenance.
Les modèles sont utilisés depuis longtemps pour construire des systèmes complexes, dans
pratiquement tous les domaines de l'ingénierie. C'est parce qu'ils fournissent une aide
inestimable pour prendre des décisions de conception importantes avant la mise en oeuvre du
système.
Dans une activité classique d’Ingénierie Dirigée par les Modèles (IDM), les systèmes sont
modélisés à l’aide d’une notation semi-formelle et sont par la suite validés puis implantés.
L’étape de validation, basée sur ces modèles, est particulièrement cruciale pour les Systèmes
Embarqués Temps-Réel (SETR), afin de s’assurer de leur bon fonctionnement. Cependant, une
démarche IDM reste insuffisante dans le sens où elle n’indique pas comment utiliser les modèles
pour appliquer l’analyse. Face à cette situation, l’intégration de méthodes formelles dans les
cycles de développement de ces systèmes est devenue primordiale. Ces méthodes sont depuis
longtemps reconnues afin d’aider au développement de systèmes fiables, en raison de leurs
fondements mathématiques, réputés rigoureux sur l’exhaustivité de la vérification formelle
qu’ils permettent de l’activer.
Dans cette thèse, nous proposons une approche basée sur la transformation de modèle pour
obtenir une spécification formelle de notre système, puis utilisons les techniques de vérification
formelles pour prouver que la conception de tel système est correcte par rapport à sa
spécification. Nous commençons par l’utilisation de diagramme d'états-transitions (Statechart),
qui décrit un système temps réel, comme modèle source pour générer un code RT-Maude, ce
code représente le module Maude du système temps réel (modèle cible). La deuxième partie de
notre travail est de ; en se basant sur le module généré ; vérifier le système par rapport aux
propriétés exprimées en logique temporelle linéaire (LTL) en utilisant Maude LTL Model-
Checker. En outre, nous utilisons RT-Maude pour rechercher et analyser le système pour
trouver des comportements indésirables. L'approche est illustrée à travers trois études de cas
Application and Use of Multivariate Control Charts In a BTA Deep Hole Drilling Process
No full textDeep hole drilling methods are used for producing holes with a high length-to-diameter ratio, good surface finish and straightness. The process is subject to dynamic disturbances usually classified as either chatter vibration or spiralling. In this paper, we will focus on the application and use of multivariate control charts to monitor the process in order to detect chatter vibrations. The results showed that chatter is detected and some alarm signals occurs at time points which can be connected to physical changes of the process. --
Usage de ChatGPT dans le milieu estudiantin en contexte algérien : entre éthique et anéthique !
No full textL\u27enseignement-apprentissage des langues étrangères, notamment le français, a connu de profondes transformations grâce aux avancées technologiques. La présente étude explore l\u27impact révolutionnaire de la numérisation et de l\u27intelligence artificielle (désormais IA), en particulier ChatGPT, dans la didactique du français comme langue étrangère. Partant d’un corpus de 333 étudiants de différents niveaux à l’université de Bordj Bou Arreridj (département de français), cette étude examine comment des outils tels que ChatGPT peuvent enrichir les expériences d\u27apprentissage, personnaliser le parcours éducatif et fournir un feedback adapté aux besoins individuels des étudiants. À travers une approche quantitative, nous analysons l\u27utilisation de ChatGPT par les étudiants, les motivations derrière cet usage ainsi que les implications éthiques liées à l’usage de l\u27IA. Notre objectif, à travers cette recherche, est de suggérer des pistes de réflexion pour une intégration efficace de ChatGPT dans les programmes éducatifs, misant sur l\u27importance des formations spécifiques ainsi que la sensibilisation aux enjeux éthiques afin de préserver l’intégrité académique. En examinant les nouvelles opportunités offertes par l\u27IA, cette étude ambitionne également à contribuer au renouvellement des approches pédagogiques en didactique du FLE
A Deep Learning Approach Based on Interpretable Feature Importance for Predicting Sports Results
No full textFootball match result prediction is a challenging task that has been the subject of much research. Traditionally, predictions have been made by team managers, fans, and analysts based on their knowledge and experience. However and recently there has been an increased interest in predicting match outcomes using statistical techniques and machine learning. These algorithms can learn from historical data to identify complex relationships between different variables, and then make predictions about the outcome of future matches. Accordingly, forecasting plays a pivotal role in assisting managers and clubs in making well-informed decisions geared toward securing victories in leagues and tournaments. In this paper, we presented an approach, which is generally applicable in all areas of sports, to forecast football match results based on three stages. The first stage involves identifying and collecting the occurred events during a football match. As a multiclass classification problem with three classes, each match can have three possible outcomes. Then, we applied multiple machine learning algorithms to compare the performance of those different models, and choose the one that performs the best. As a final step, this study goes through the critical aspect of model interpretability. We used the SHapley Additive exPlanations (SHAP) method to decipher the feature importance within our best model, focusing on the factors that influence match predictions. Experiment results indicate that the Multilayer Perceptron (MLP), a neural network algorithm, was effective when compared to various other models and produced competitive results with prior works. The MLP model has achieved 0.8342 for accuracy. The particular significance of this study lies in the use of the SHAP method to explain the predictions made by the MLP model. Specifically, by exploiting its graphical representation to illustrate the influence of each feature within our dataset in predicting the outcome of a football match
A Model Transformation Approach for Specifying Real-Time Systems and Its Verification Using RT-Maude
No full textReal-time systems must be properly validated and verified before their manufacturing and deployment in order to increase their reliability and reduce their maintenance cost. Models have been used for a long time to build complex systems, in virtually every engineering field. This is because they provide invaluable help in making important design decisions before the system is implemented. In this paper, the authors propose an approach based on model transformation to apply formal verification techniques to demonstrate the correctness of system designs. At the first step, they describe real-time systems by state chart (machine) diagrams, as source models to generate RT-Maude models (target models). The second step is to use the result models to verify the real-time systems against specified LTL properties using Maude LTL Model-Checker. This approach is illustrated through an example.</jats:p
Thermal behavior modeling of a cabinet direct solar dryer as influenced by sensible heat storage in a fractured porous medium
No full textGlobal minimum and orthogonality in C1-classes
No full textCollege of Science, Department of Mathematics, PO Box 2455, Riyadh 11451, Saudi ArabiaIn this paper we characterize the global minimum of an arbitrary function defined on a Banach space, in terms of a new concept of derivatives adapted for our case from a recent work due to D.J. Keckic (J. Operator Theory, submitted for publication). Using these results we establish several new characterizations of the global minimum of the map defined by Fψ(X)=ψ(X)1, where ψ :U→C1 is a map defined by ψ(X)=S+φ(X) and φ :B(H)→B(H) is a linear map, SC1, and U={XB(H): φ(X)C1}. Further, we apply these results to characterize the operators which are orthogonal to the range of elementary operators.This work is supported, for the first author, by the Research Center Project Math/1422/10 and for the second
author by the Research Center Project Math/1422/22
