Machine à états abstraits

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En informatique, une machine à états abstraits, ou abstract state machine (ASM) en anglais, est une machine fonctionnant état pour les États qui sont des structures de données arbitraires (structure dans le sens de la logique mathématique, qui est un ensemble non vide avec un certain nombre de fonctions (opérations sur l'ensemble) et relations).


La méthode ASM est une méthode de pratiques et scientifiquement des Ingénierie des systèmes qui comble le fossé entre les deux extrémités du développement du système:

  • l'entendement humain et la formulation des problèmes du monde réel (Analyse des exigences en utilisant précis de haut niveau de modélisation à l'échelle de l'abstraction déterminée par le domaine d'application donné).
  • le déploiement de leurs solutions algorithmiques par code-exécution de machines sur l'évolution des plates-formes (définition des décisions de conception, de mise en œuvre du système et les détails).

La méthode repose sur trois concepts fondamentaux:

  • ASM: une forme précise de pseudo-code, généralisant Automate fini pour fonctionner sur des structures de données arbitraires.
  • modèle de fondement: une forme rigoureuse des plans, servant de modèle de référence faisant autorité pour la conception.
  • raffinement: un schéma plus général pour instanciations pas à pas des abstractions du modèle à des éléments concrets du système, qui relie contrôlables entre les descriptions de plus en plus détaillées aux étapes successives du développement du système.

Dans la conception originale de ASM, un seul agent exécute un programme dans une séquence d'étapes, éventuellement interagir avec son environnement. Cette notion a été étendue pour capturer calculs distribués, dans lequel plusieurs agents exécutent leurs programmes en même temps.

Depuis algorithmes du modèle de ASM à des niveaux arbitraires de l'abstraction, ils peuvent fournir de haut niveau et de bas niveau et de niveau intermédiaire vues d'un matériel ou logiciel de conception. Spécifications de ASM sont souvent constitués d'une série de modèles de ASM, à commencer par un modèle de terrain abstrait et de procéder à de plus grands niveaux de détail dans raffinement successifs ou coarsenings.

En raison de la nature algorithmique et mathématiques de ces trois concepts, modèles de ASM et leurs propriétés d'intérêt peuvent être analysées en utilisant toute forme rigoureuse de vérification (par le raisonnement) ou de validation (par l'expérimentation, les tests exécutions du modèle).

Histoire[modifier | modifier le code]

Le concept de l'ASM est due à Yuri_Gurevich, qui le premier a proposé au milieu des années 1980 comme un moyen d'améliorer la thèse de Turing que chaque algorithme est simulée par une Machine de Turing appropriée. Il a formulé la thèse de l'ASM: chaque algorithme, quel que soit abstraite, étape par étape émulé par un ASM appropriée. En 2000, Gurevich axiomatisé la notion d'algorithmes séquentiels, est prouvé la thèse de l'ASM pour eux. En gros, les axiomes sont les suivants: les États sont des structures, la transition d'état ne porte que sur une partie limitée de l'État, et tout ce qui est invariant par isomorphisme de structures. (Les structures peuvent être considérées comme des algèbres, ce qui explique le nom original évolution algèbres de ASM.) L'axiomatisation et la caractérisation des algorithmes séquentiels ont été étendus aux algorithmes parallèles et interactifs.

Dans les années 1990, par un effort de la communauté, la méthode ASM a été mis au point, en utilisant ASM pour la spécification formelle et de l'analyse (vérification et validation) de matériel informatique et de logiciels. Spécifications complètes de l'ASM de Langage de programmation (y compris Prolog, C et Java) et les language de conception (UML et SDL) ont été développés. Un historique détaillé peut être trouvé dans le AsmBook] (chapitre 9) ou dans le présent article.

Un certain nombre d'outils logiciels pour l'exécution ASM et l'analyse sont disponibles.

Bibliographie[modifier | modifier le code]

Livres[modifier | modifier le code]

Modèles de comportement pour les normes industrielles[modifier | modifier le code]

Outils[modifier | modifier le code]

(par ordre chronologique depuis le 20

Références[modifier | modifier le code]

Liens externes[modifier | modifier le code]