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.

Pour les articles homonymes, voir 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)[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.

Notes et références
  1. Yuri Gurevich, « A New Thesis », Abstracts, American Mathematical Society Vol. 6, n° 4, août 1985), page 317, abstract 85T-68-203.
  2. Yuri Gurevich, « Sequential abstract-state machines capture sequential algorithms », ACM Transactions on Computational Logic, Association for Computing Machinery (ACM), vol. 1, no 1,‎ , p. 77-111 (DOI 10.1145/343369.343384, lire en ligne).
  3. Egon Börger et Dean Rosenzweig, « A mathematical definition of full Prolog », Science of Computer Programming, vol. 24, no 3,‎ , p. 249-286 (DOI 10.1016/0167-6423(95)00006-e)
  4. Egon Börger, Nicu G. Fruja, Vincenzo Gervasi et Robert F. Stärk, « A high-level modular definition of the semantics of C# », Theoretical Computer Science, vol. 336, nos 2-3,‎ , p. 235-284 (ISSN 0304-3975, DOI 10.1016/j.tcs.2004.11.008).
  5. Robert F. Stärk, Joachim Schmid et Egon Börger, Java and the Java Virtual Machine : Definition, Verification, Validation, Springer, , 381 p. (ISBN 978-3-540-42088-0).
  6. Uwe Glässer, Reinhard Gotzhein et Andreas Prinz, « The formal semantics of SDL-2000: Status and perspectives », Computer Networks, vol. 42, no 3,‎ , p. 343-358 (ISSN 1389-1286, DOI 10.1016/s1389-1286(03)00247-0).
  7. Robert Eschbach, Uwe Glässer, Reinhard Gotzhein, Martin von Löwis et Andreas Prinz, « Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models », Journal of Universal Computer Science, vol. 7, no 11,‎ (lire en ligne).
  8. Egon Börger, Uwe Glässer et Wolfgang Muller, « A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines », dans Carlos Delagado Kloos et Peter T. Breuer (éditeurs), Formal Semantics for VHDL, Springer, (DOI 10.1007/978-1-4615-2237-9_5), p. 107-139

Bibliographie
  • Yuri Gurevich, « Evolving Algebras 1993: Lipari Guide », dans Egon Börger, Specification and validation methods, Oxford University Press, USA, , 460 p. (ISBN 0-19-853854-5), p. 9-36
  • (en) Egon Börger et Robert F. Stärk, Abstract State Machines : A Method for High-level System Design and Analysis ; with 19 Tables, Springer Science & Business Media, , 438 p. (ISBN 978-3-540-00702-9, lire en ligne).
  • Yuri Gurevich, Philipp W. Kutter, Martin Odersky et Lothar Thiele, Abstract State Machines : Theory and Applications : International Workshop, ASM 2000 Monte Verita, Switzerland, March 19-24, 2000 Proceedings, Springer Science & Business Media, coll. « Lecture Notes in Computer Science » (no 1912), , 386 p. (ISBN 978-3-540-67959-2).
  • Andreas Glausch Abstract-State Machines Eine Sammlung didaktischer Beispiele, . — Une collection d'exemples
  • Egon Börger Abstract State Machines — Une introduction

Implémentations

Liens externes
  • Portail de l’informatique
  • Portail de l'informatique théorique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.