Macchina a stati astratta

In informatica , una macchina a stati astratti ( macchine a stati astratte in inglese o ASM ) è un automa finito i cui stati non hanno solo nomi, ma strutture nel senso della logica matematica , vale a dire insiemi non vuoti con funzioni , operazioni e relazioni . Le strutture possono essere viste come algebre, il che spiega il nome di algebre evolutive inizialmente dato agli ASM.

I principi

Il metodo ASM è un metodo pratico e scientificamente fondato di ingegneria dei sistemi che collega i due aspetti dello sviluppo del sistema:

Il metodo si basa su tre concetti:

Inizialmente, gli ASM sono progettati per un singolo agente ; il concetto è stato successivamente esteso ai calcoli distribuiti , in cui più agenti eseguono i propri programmi contemporaneamente. L' ASM modella gli algoritmi a livelli arbitrari di astrazione. Possono quindi fornire descrizioni di alto livello, medio o basso livello. Le specifiche ASM sono spesso costituite da una suite di modelli ASM , a partire da un modello di base astratto e procedendo a livelli più dettagliati mediante perfezionamenti successivi.

A causa della natura algoritmica e matematica di questi tre concetti, i modelli ASM e le loro proprietà possono essere analizzati utilizzando qualsiasi metodo rigoroso di verifica (ragionamento) o validazione (mediante sperimentazione e test di esecuzione del modello).

Applicazioni

Nella compilazione , il modello viene utilizzato per la descrizione della semantica e quindi aiuta a garantire la conservazione di questa semantica durante la traduzione. Più in generale, il modello consente, in fase di analisi e progettazione dello sviluppo software, una descrizione formale dei requisiti funzionali. L'approccio matematico migliora la verifica e il riutilizzo. La formalizzazione degli stati astratti viene utilizzata anche quando si progettano circuiti complessi in logica sequenziale .

Evoluzione del modello

Gli ASM furono introdotti a metà degli anni '80 da Yuri Gurevich  (in) di Microsoft, che li offrì come mezzo per raggiungere la tesi della Chiesa , secondo cui qualsiasi algoritmo può essere simulato da una macchina di Turing vera e propria. Gurevich lo ha formulato nella forma che è diventata la "Tesi ASM"  : qualsiasi algoritmo, qualunque sia il suo livello di astrazione , può essere oggetto di una progressiva emulazione da parte di un appropriato ASM. Nel 2000, Gurevich ha fornito un'assiomatizzazione della nozione di algoritmo sequenziale e ha dimostrato la "tesi ASM" per questa classe. Gli assiomi sono - grosso modo - la seguente: stati sono strutture, e una transizione di stato riguarda solo una parte limitata dello stato, e infine tutto è invariante da isomorfismo di strutture. L'assiomatizzazione e la caratterizzazione degli algoritmi sequenziali sono state poi estese ad algoritmi paralleli e interattivi.

Negli anni '90, il metodo ASM è stato utilizzato nella specifica formale , verifica e convalida di hardware e software . Le specifiche complete in ASM sono sviluppate per linguaggi di programmazione come Prolog , C e Java e linguaggi di progettazione come UML e SDL o VHDL . Una storia dettagliata può essere trovata nel capitolo 9 del libro Abstract State Machines , 2003 o nell'articolo di Egon Börger, "  Le origini e lo sviluppo del metodo ASM ad alto livello  ", Journal of Universal Computer Science , vol.  8, n o  1,2002( leggi online ). Sono disponibili numerosi strumenti software per l'analisi e l'esecuzione degli ASM.

Note e riferimenti

  1. Yuri Gurevich, "A New Thesis", Abstracts, American Mathematical Society Vol. 6, n. 4, agosto 1985), pagina 317, abstract 85T-68-203.
  2. Yuri Gurevich, "  Le macchine sequenziali a stati astratti acquisiscono algoritmi sequenziali  ", ACM Transactions on Computational Logic , Association for Computing Machinery (ACM), vol.  1, n o  1,luglio 2000, p.  77-111 ( DOI  10.1145 / 343369.343384 , leggi online ).
  3. Egon Börger e Dean Rosenzweig, "  Una definizione matematica del prologo completo  ", Science of Computer Programming , vol.  24, n o  3,Giugno 1995, p.  249-286 ( DOI  10.1016 / 0167-6423 (95) 00006-e )
  4. Egon Börger, Nicu G. Fruja, Vincenzo Gervasi e Robert F. Stärk, "  A high-level modular definition of the semantics of C #  ", Theoretical Computer Science , vol.  336, n osso  2-3,Maggio 2005, p.  235-284 ( ISSN  0304-3975 , DOI  10.1016 / j.tcs.2004.11.008 ).
  5. Robert F. Stärk, Joachim Schmid e Egon Börger, Java and the Java Virtual Machine: Definition, Verification, Validation , Springer,2001, 381  p. ( ISBN  978-3-540-42088-0 ).
  6. Uwe Glässer, Reinhard Gotzhein e Andreas Prinz, "  The formal semantics of SDL-2000: Status and perspectives  ", Computer Networks , vol.  42, n o  3,Giugno 2003, 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 e Andreas Prinz, "  Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models  ", Journal of Universal Computer Science , vol.  7, n o  11, 2001( leggi online ).
  8. Egon Börger, Uwe Glässer e Wolfgang Muller, "A Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines" , in Carlos Delagado Kloos e Peter T. Breuer (a cura di), Formal Semantics for VHDL , Springer,1995( DOI  10.1007 / 978-1-4615-2237-9_5 ) , p.  107-139

Bibliografia

Implementazioni

link esterno