# Machine à états abstraits

En informatique, une machine à états abstraits (en anglais abstract state machine ou ASM), est un automate fini dont les états ne portent pas simplement des noms, mais des structures au sens de la logique mathématique, c'est-à-dire des ensembles non vides munis de fonctions, d'opérations et de relations. Les structures peuvent être vues comme des algèbres, ce qui explique le nom d'algèbres évolutives donné initialement aux ASM.

## Principes

La méthode des ASM est une méthode d'ingénierie des systèmes pratique et scientifiquement fondée qui jette un pont entre les deux aspects du développement d'un système:
* d'une part la formulation, en termes compréhensibles par un humain, de problèmes du monde réel : analyse des exigences par une modélisation de haut niveau d'abstraction du domaine d'application ;
* d'autre part le déploiement des solutions algorithmiques sur des plates-formes variées : définition des décisions de conception, des détails d'implémentation et de système.
La méthode repose sur trois concepts :
* les ASM , qui sont une forme précise de pseudo-code, généralisant les automates finis et qui opèrent sur des structures de données arbitraires.
* les modèles de base : un ensemble des modèles qui servent de référence pour la conception.
* le raffinement : un schéma général pour une instanciation progressive, mécanisme contrôlable entre les descriptions des étapes successives du développement du système.
Initialement, les ASM, sont conçues pour un seul agent; le concept a ensuite été étendue aux calculs distribués, où plusieurs agents exécutent leurs programmes simultanément. Les ASM modélisent les algorithmes à des niveaux arbitraires de l'abstraction. Ils peuvent donc fournir des descriptions de haut niveau , de niveau intermédiaire ou de bas niveau. Les spécifications ASM sont souvent constituées d'une suite de modèles ASM, commençant par un modèle de base abstrait et procédant vers des niveaux plus détaillés par raffinements successifs.
En raison de la nature algorithmique et mathématique de ces trois concepts, les modèles ASM et leurs propriétés peuvent être analysés en utilisant toute méthode rigoureuse de vérification (par raisonnement) ou de validation (par expérimentation et tests d'exécution du modèle).

## Applications

En compilation, le modèle sert à la description de la sémantique et aide ainsi à assurer la préservation de cette sémantique durant la traduction. Plus généralement le modèle permet, durant la phase d'analyse et de conception du développement de logiciels, une description formelle des exigences fonctionnelles. La démarche mathématique améliore la vérification et la réutilisation. On utilise la formalisation des états abstraits aussi lors de la conception de circuits complexes en logique séquentielle.

## Évolution du modèle

Les ASM ont été introduites au milieu des années 1980 par Yuri Gurevich (en) de Microsoft, qui les a proposées comme un moyen de réaliser la thèse de Church, selon laquelle tout algorithme peut être simulé par une machine de Turing appropriée. Gurevich l'a formulé sous la forme devenue la « thèse ASM » : tout algorithme, quel que soit son niveau d'abstraction, peut faire l'objet d'une émulation progressive par une ASM appropriée. En 2000, Gurevich donne une axiomatisation de la notion d'algorithme séquentiel, et démontre la « thèse ASM » pour cette classe. Les axiomes sont — grosso modo — les suivants: les états sont des structures, et une transition d'état ne porte que sur une partie limitée de l'état, et enfin tout est invariant par isomorphisme de structures. L'axiomatisation et la caractérisation des algorithmes séquentiels ont été étendus ensuite aux algorithmes parallèles et interactifs.
Dans les années 1990, la méthode ASM est utilisée dans la spécification formelle, la vérification et la validation de matériels et de logiciels. Des spécifications complètes en ASM sont développées pour des langages de programmation comme Prolog, C et Java, et des langages de conception comme UML et SDL)$^,$ ou VHDL. Un historique détaillé peut être trouvé dans le chapitre 9 du livre Abstract State Machines, 2003 ou dans l'article d'Egon Börger, « The origins and the development of the ASM method for high level », Journal of Universal Computer Science, vol. 8, n$^o$ 1,‎ 2002 (lire en ligne). Un certain nombre d'outils logiciels pour l'analyse et l'exécution des ASM sont disponibles.