Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Vérification de modèles
Résumé
thumb|308x308px|Principe du model checking.
En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique. Sur le plan pratique, la vérification de modèles est devenue, au niveau industriel, la méthode de vérification de code et de systèmes matériels la plus populaire et la plus utilisée aujourd'hui.
La vérification de modèles s'appuie sur la logique temporelle dont l'un des pionniers est Amir Pnueli, qui reçut le prix Turing en 1996 pour (). Le model checking commence avec les travaux d'Edmund M. Clarke, E. Allen Emerson, Jean-Pierre Queille
et Joseph Sifakis au tout début des années 1980. Clarke, Emerson et Sifakis se sont vu attribuer le prix Turing 2007 pour leurs travaux sur le model checking.
Dans cette section, on précise ce que l'on entend par modèle et propriété puis par le problème de model checking.
thumb|378x378px|Système de transition d'états pour un distributeur de boissons.
Le système est modélisé par un système de transition d'états. Il s'agit d'un graphe orienté : un sommet représente un état du système et chaque arc représente une transition, c'est-à-dire une évolution possible du système d'un état donné vers un autre état. Chaque état du graphe orienté est étiqueté par l'ensemble des propositions atomiques vraies à ce point d'exécution (par exemple, i=2, le processeur 3 est en attente). Un tel graphe est aussi appelé une structure de Kripke.
On donne ici l'exemple d'un distributeur de boissons qui peut être dans 4 états : attente d'une pièce de monnaie, sélection d'une boisson, distribution d'une bouteille d'eau minérale et distribution d'une bouteille de jus d'orange.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Concepts associés (18)
Vérification formelle
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Logique temporelle linéaire
En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin.
Réseau de Petri
Animated_Petri_net_commons.gif Un réseau de Petri (aussi connu comme un réseau de Place/Transition ou réseau de P/T) est un modèle mathématique servant à représenter divers systèmes (informatiques, industriels...) travaillant sur des variables discrètes. Les réseaux de Petri sont apparus en 1962, dans la thèse de doctorat de Carl Adam Petri. Les réseaux de Petri sont des outils graphiques et mathématiques permettant de modéliser et de vérifier le comportement dynamique des systèmes à événements discrets comme les systèmes manufacturiers, les systèmes de télécommunications, les réseaux de transport.