Runtime Verification of Real-Time Applications Using Trace Data and Model Requirements
Bibliographic record
Abstract
x aux évènements ou listes d'évènements qui étaient attendus, afin de mettre en avant les discordances.Avec notre structure, une fois qu'une trace a été analysée, nous obtenons une liste d'instances de l'application qui suivent le modèle défini.Ces instances contiennent le détail de leurs étapes, ce qui correspond à une liste ordonnée des états du modèle rencontrés, ainsi que les évènements qui ont enclenché chaque transition.Une étape de l'instance contient ellemême les informations sur toutes les contraintes qui ont été vérifiées à cette étape, ainsi que l'étape à laquelle la variable utilisée dans la contrainte a été initialisée pour la dernière fois.Il est donc possible d'identifier l'ensemble des étapes d'instances similaires pour lesquelles une contrainte était concernée, et de séparer les cas où cette contrainte était valide de ceux où elle était invalide.Les cas où la validation était incertaine sont mis de côté, étant donné que nous ne pouvons être sûrs de quel serait le statut de l'étape d'instance en question.Les étapes d'instance étant considérées par contrainte, il est tout à fait possible qu'une instance qui était invalide pour une contrainte soit considérée comme valide pour une autre.Pour chaque contrainte pour laquelle au moins un cas était invalide, on lancera donc le processus d'analyse.Cependant, comme beaucoup d'instances peuvent être dans les traces, toutes les analyser prendrait du temps.Nous utilisons donc de l'échantillonnage avec sélection aléatoire de l'échantillon pour limiter le nombre d'instances à analyser.Cet échantillonnage sera appliqué d'un côté pour les instances valides, et de l'autre pour les instances invalides.Pour les instances sélectionnées, il est nécessaire d'identifier les éléments clés, ou éléments d'intérêt, qui donneront les informations nécessaires pour déterminer l'origine du problème.Ces éléments diffèrent selon le type de la variable utilisée pour la contrainte.Les compteurs et les minuteurs utiliseront ainsi les données sauvegardées dans le système d'états.Ceci permet de directement faire une recherche pour les dates auxquelles la valeur de la variable a changé au cours de l'instance étudiée.Une fois ces estampilles de temps obtenues, nous pouvons directement lire depuis la trace les évènements qui ont provoqué ces changements de valeur, et en extraire les informations souhaitées.Cette information pourrait par exemple être le nom de l'appel système pour un compteur d'appels système, ou le statut du processus reporté pour un minuteur d'usage du processeur.En ce qui concerne les variables indépendantes, les éléments clés sont tous ceux qui pourraient avoir une influence sur la valeur de cette variable.Par exemple, dans le cas d'une variable de date limite, nous avons créé un attribut dans le système d'états qui suit l'état du processus tout au long de la trace.Ainsi, chaque changement d'état du processus pendant la période est extrait comme étant un élément d'intérêt.Les éléments d'intérêt ainsi extraits seront par la suite stockés comme des durées d'élément.Chaque durée d'élément contient l'élément ainsi que l'incrément causé par l'apparition de xi cet élément à ce moment.Toutes les durées trouvées pendant une période de temps sont par la suite agrégées dans un ensemble de durées d'élément.Cet ensemble contient ainsi un certain nombre de durées qui peuvent ou non concerner un même élément.Un ensemble peut être vide, ce qui signifie qu'aucun élément n'a été trouvé pendant la période analysée.Pour une liste d'instances, les ensemble de durées d'élément similaires sont ensuite réunis dans un ensemble d'intervalles d'élément.On considère deux ensembles de durées comme étant similaires s'ils partagent la même configuration de clés, c'est-à-dire le même nombre de durées concernant les mêmes éléments.Lorsqu'on agrège des ensembles de durées dans des ensembles d'intervalles, on considère simplement leur contenu et non leur ordre d'apparition sur la période.Ainsi, lorsqu'on crée un ensemble d'intervalles à partie d'un ensemble de durées, on obtient un nombre d'intervalles avec des valeurs minimum et maximum identiques, correspondant aux différentes durées de l'ensemble d'origine.Lorsqu'on agrège un ensemble de durées dans un ensemble d'intervalles existant, les durées de l'ensemble de durées seront appariées avec les intervalles de l'ensemble d'intervalles dans le but de garder les intervalles résultats aussi petits que possible.Si les ensembles de durée utilisés pour former un ensemble d'intervalles sont vides, alors ce dernier sera vide aussi.L'étape d'analyse termine par l'attribution des responsabilités aux éléments extraits pour identifier clairement les éléments qui ont le plus à voir avec la violation de la contrainte.Deux algorithmes sont utilisés selon le type et la valeur de la contrainte utilisée.Si la contrainte est absolue, autrement dit si n'importe quel changement à la valeur de la variable pendant la période analysée est prohibé, on choisira l'algorithme d'analyse partielle pour calculer directement les responsabilités pour tous les éléments qui ont mené à un changement de valeur.On assignera donc les responsabilités minimum et maximum pour chaque élément comme étant leur pourcentage d'implication dans respectivement le minimum total et le maximum total de l'ensemble d'intervalle.On calculera ensuite la responsabilité d'un élément comme étant la moyenne de ces deux valeurs.Dans le cas où la contrainte n'est pas absolue, c'est-à-dire que des changements à la valeur de la variable sont utilisés, l'algorithme d'analyse complète est nécessaire afin de réaliser la comparaison des ensembles car on ne peut pas considérer directement qu'un élément fait partie du problème.Ainsi, on identifie les différents cas valides et invalides représentés par des ensembles d'intervalles d'élément.Pour chacun des cas invalides, la distance à chaque cas valide est calculée, et un poids de proximité leur est associé.Ce sont les cas valides aux poids les plus élevés qui seront ensuite utilisés afin de les soustraire à l'intervalle invalide traité.Cette soustraction se fait selon l'opérateur utilisé pour la contrainte, et retourne un ensemble différentiel d'intervalles local.Si plusieurs ensemble différentiels locaux sont obtenus, ils sont agrégés selon un processus appelé « inter-union » qui fait une intersection sur les éléments contenus, et une union sur xii les valeurs des intervalles.Ce processus permet d'éliminer des éléments qui pourraient être considérés comme problématiques dans un cas, mais qui ne le sont pas dans un autre, tout en élargissant les intervalles si nécessaire.Finalement, on calcule la responsabilité locale d'un élément par rapport à son pourcentage d'implication dans l'intervalle différentiel local.Si plusieurs instances invalides aux configurations de clés différentes ont été découvertes, ces responsabilités locales seront alors réunies pour former la responsabilité globale de chaque élément concerné.Le diagnostic peut enfin être posé en utilisant les responsabilités calculées.Certains cas cependant nécessitent des analyses plus précises.Lorsque l'un de ces cas a une responsabilité élevée, les analyses correspondantes seront automatiquement déclenchées.Les résultats de ces analyses passeront ensuite au travers des mêmes algorithmes afin d'affiner le résultat présenté à l'utilisateur.La dernière partie de l'automatisation du processus consiste à automatiser la génération du modèle à partir de la trace.Afin de déterminer premièrement le déroulement de l'application, c'est-à-dire ses états et transitions, il faut analyser la trace de l'espace utilisateur qui contient les évènements générés par l'application.Cependant, les évènements dans la trace de l'espace utilisateur peuvent concerner de multiples applications et processus.Les modèles utilisés pour l'analyse suivent des processus, il est donc important d'identifier les différents déroulements selon les processus impliqués.Pour cela, la première phase consiste à organiser les évènements de la trace par fil d'exécution, tout en conservant leur ordre d'apparition.Il est possible que plusieurs fils d'exécution partagent le même déroulement d'exécution.Ainsi, en utilisant un algorithme de plus longue sous-séquence commune sur les séquences d'évènements des processus, on peut les regrouper en un nombre limité de déroulements communs.Comme les évènements peuvent contenir des différences au niveau de leur contexte que l'on pourrait vouloir éliminer, comme par exemple une information sur le numéro de processus pour une application multi-processus, on a défini un taux minimum de regroupement qui, lorsqu'il n'est pas atteint, réduit les contraintes d'identité pour associer les évènements.Ce comportement n'est effectif que si le taux de regroupement idéal -lorsque l'on ne considère que les noms des évènements et pas leur contenu -atteint le taux minimum de regroupement.xv intéressant de profiter du mode enregistreur de vol de LTTng afin de fournir une détection « en direct » des problèmes que l'on pourrait rencontrer.Il serait ainsi possible, pendant que l'application s'exécute, de construire le modèle, démarrer la détection, prendre un instantané de la trace en cas de contrainte invalide, et analyser l'origine du problème dans la trace ainsi obtenue.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.010 | 0.052 |
| Meta-epidemiology (narrow) | 0.002 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.002 | 0.001 |
| Science and technology studies | 0.001 | 0.002 |
| Scholarly communication | 0.003 | 0.005 |
| Open science | 0.003 | 0.002 |
| Research integrity | 0.001 | 0.002 |
| Insufficient payload (model declined to judge) | 0.002 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".