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, « A New Thesis », Abstracts, American Mathematical Society Vol. 6, n° 4, août 1985), page 317, abstract 85T-68-203. 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 ou dans l'article d'. Un certain nombre d'outils logiciels pour l'analyse et l'exécution des ASM sont disponibles. Notes et références
Bibliographie
. . Andreas Glausch Abstract-State Machines Eine Sammlung didaktischer Beispiele, . — Une collection d'exemples Egon Börger Abstract State Machines — Une introduction
Implémentations
Abstract State Machine Language sur Microsoft Research ASMETA, the Abstract State Machine Metamodel and its tool set AsmL sur CodePlex The CoreASM Project The TASM toolset: specification, simulation, and formal verification of real-time systems
Liens externes AsmCenter Abstract State Machines – Site d'information Liste des conférences ASM – ASM sur dblp
Catégorie:Informatique théorique Catégorie:Méthode formelle