Introduction

Valider formellement un algorithme permet, de s’assurer que le design ne contient pas de faute de logique. Pour de petits algorithmes, il est plutôt simple d’avoir en tête la liste de tous les états possibles du systèmes. Mais lorsque l’on prend en compte de la concurrence ainsi que du non-déterminisme rajouté par le réseau, ce n’est pas possible d’avoir en tête l’entièreté des états possibles du système. La Vérification Formelle est le fait de prouver l’exactitude d’un système par rapport à une spécification formelle et des propriétés, utilisant des méthodes formelles mathématiques. Il existe différents types de vérification formelle, certaines permettent de vérifier des algorithmes, d’autres des implémentations. ...

Formally validating an algorithm ensures that the design does not contain any logical errors. For small algorithms, it is fairly simple to keep track of all possible states of the system. However, when concurrency and non-determinism added by the network are taken into account, it is not possible to keep track of all possible states of the system. Formal verification is the process of proving the correctness of a system against a formal specification and properties, using formal mathematical methods. There are different types of formal verification, some of which can be used to verify algorithms, others to verify implementations. ...

RDF Le Ressource Description Framework (RDF) est un standard du W3C1 pour représenter de la connaissance sous forme de graphe. Multigraphe signifie qu’il peut comporter des boucles et des arêtes multiples. Orienté signifie que les signifie que les arêtes ont un sens. Étiqueté signifie que les arêtes ainsi que les sommets portent une étiquette Un Multigraphe orienté étiqueté Triple RDF Les graphes RDF sont représentés avec des triples RDF au format Sujet - Prédicat - Objet, ou plutôt « S ; P ; O » (sujet pour le nœud de départ, prédicat pour l’arête et objet pour le nœud de destination). ...

RDF The Resource Description Framework (RDF) is a W3C1 standard for representing knowledge in graph form. Multigraph means that it can contain loops and multiple edges. Directed means that the edges have a direction. Labeled means that both the edges and the vertices have a label. A labeled directed multigraph RDF triples RDF graphs are represented with RDF triples in the format Subject - Predicate - Object, or rather « S ; P ; O » (subject for the starting node, predicate for the edge, and object for the destination node). ...

The goal of this analysis The goal of this analysis is to find useful feedback for Flight Comparator Applications. We want to find a way to extract UX related feedback from a huge pool of reviews, we’ll do this analysis on the Skyscanner and Kayak applications. Quick remarks We can’t really retrieve all the reviews for an app that we aren’t the owner of, but I managed to extract a reasonable amount of reviews for both of the applications (about 50K reviews each). ...