Loading AI tools
Modèle mathématique de calcul qui opère sur des états de structures mathématiques De Wikipédia, l'encyclopédie libre
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.
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:
La méthode repose sur trois concepts :
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).
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.
Les ASM ont été introduites au milieu des années 1980 par Yuri Gurevich (en)[1] 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[2]. 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[3], C[4] et Java[5], et des langages de conception comme UML et SDL)[6],[7] ou VHDL[8]. 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, no 1, (lire en ligne). Un certain nombre d'outils logiciels pour l'analyse et l'exécution des ASM sont disponibles.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.