Système Maude - Maude system

Le système Maude est une implémentation de la logique de réécriture . Il est similaire dans son approche générale de Joseph Goguen de OBJ3 mise en œuvre de la logique équationnelle , mais basée sur la logique de réécriture plutôt que l' ordre trié logique équationnelle , et avec un accent sur la puissante metaprogramming basée sur la réflexion .

Maude est un logiciel gratuit et des tutoriels sont disponibles en ligne. Il a été développé à l'origine à SRI International , mais est maintenant développé par une collaboration diversifiée de chercheurs.

introduction

Maude se propose de résoudre un ensemble de problèmes différent des langages impératifs ordinaires comme C, Java ou Perl. C'est un outil de raisonnement formel, qui peut nous aider à vérifier que les choses sont « comme elles devraient », et nous montrer pourquoi elles ne le sont pas si c'est le cas. En d'autres termes, Maude nous permet de définir formellement ce que nous entendons par un certain concept d'une manière très abstraite (sans nous préoccuper de la façon dont la structure est représentée en interne, etc.), mais nous pouvons décrire ce que l'on pense être l'égal concernant notre théorie. ( équations ) et par quels changements d'état il peut passer ( règles de réécriture ).

Les modules Maude (théories de réécriture) consistent en un langage terminologique plus des ensembles d'équations et de règles de réécriture. Les termes d'une théorie de la réécriture sont construits à l'aide d'opérateurs (fonctions prenant 0 ou plusieurs arguments d'une sorte , qui renvoient un terme d'une sorte spécifique). Les opérateurs prenant 0 arguments sont considérés comme des constantes, et on construit leur langage terminologique par ces constructions simples. Maude permet à l'utilisateur de spécifier si les opérateurs sont ou non infixes, postfixes ou préfixes (par défaut), cela se fait en utilisant des traits de soulignement comme remplisseurs de place pour les termes d'entrée.

Les équations de réduction sont supposées confluentes et terminales. Les règles de réécriture n'ont pas cette restriction.

Lorsque Maude "exécute", elle réécrit les termes selon les équations et les règles de réécriture. Maude réécrit les termes selon les équations chaque fois qu'il y a une correspondance entre les termes fermés que l'on essaie de réécrire (ou de réduire) et le côté gauche d'une équation dans notre ensemble d'équations. Une correspondance dans ce contexte est une substitution des variables dans le membre gauche d'une équation qui la laisse identique au terme que l'on essaie de réécrire/réduire. Les équations et les règles de réécriture peuvent également être des règles conditionnelles , ce qui signifie qu'elles doivent remplir certains critères pour être appliquées au terme (autre que la correspondance avec le côté gauche de la règle de réécriture)

Les règles sont appliquées de manière "aléatoire" par le système Maude, ce qui signifie que vous ne pouvez pas être sûr qu'une règle s'applique avant une autre règle et ainsi de suite. Si une équation peut être appliquée au terme, elle sera toujours appliquée avant toute règle de réécriture. La recherche intégrée de Maude peut rechercher des états indésirables et montrer qu'aucun de ces états ne peut être atteint. Maude a la capacité de contrôler quelles applications de règles doivent être tentées à chaque étape en utilisant la méta-programmation , en raison de la propriété réfléchissante ou de la logique de réécriture.

Usage

Maude a été utilisé pour valider les protocoles de sécurité et le code critique. Le système Maude a prouvé des failles dans les protocoles de cryptographie en spécifiant simplement ce que le système peut faire, et en recherchant des situations indésirables (états ou termes qui ne devraient pas être possibles à atteindre), le protocole peut être montré pour contenir des bogues, pas des bogues de programmation mais des situations se produisent qui sont difficiles à prévoir simplement en empruntant le "chemin du bonheur" comme le font la plupart des développeurs.

Les références

Lectures complémentaires

Liens externes