Abstraktní stavový automat - Abstract state machine

v počítačová věda, an abstraktní stavový stroj (ASM) je státní stroj pracuje na státy což jsou libovolné datové struktury (struktura ve smyslu matematická logika, to je neprázdné soubor společně s řadou funkce (operace ) a vztahy přes sadu).

The Metoda ASM je praktický a vědecky podložený systémové inženýrství metoda, která překlenuje mezeru mezi dvěma konci vývoje systému:

  • lidské chápání a formulace problémů reálného světa (zachycení požadavků přesným modelováním na vysoké úrovni na úrovni abstrakce určené danou doménou aplikace)
  • nasazení jejich algoritmických řešení stroji provádějícími kód na měnících se platformách (definice návrhových rozhodnutí, podrobnosti systému a implementace).

Metoda vychází ze tří základních konceptů:

  • ASM: přesná forma pseudokódu, zobecňující Konečné státní stroje pracovat nad libovolnými datovými strukturami
  • pozemní model: důsledná forma plánů sloužících jako autoritativní referenční model pro návrh
  • upřesnění: nejobecnější schéma postupných instancí modelových abstrakcí ke konkrétním prvkům systému, poskytující kontrolovatelné vazby mezi stále podrobnějším popisem v postupných fázích vývoje systému.

V původním pojetí ASM, jediný činidlo provádí program v posloupnosti kroků, případně interagujících s jeho prostředím. Tato představa byla rozšířena o zachycení distribuované výpočty, ve kterém více agentů spouští své programy současně.

Vzhledem k tomu, že ASM modelují algoritmy na libovolných úrovních abstrakce, mohou poskytovat pohledy na návrh hardwaru nebo softwaru na vysoké, nízké a střední úrovni. Specifikace ASM se často skládají z řady modelů ASM, počínaje abstraktem pozemní model a postupovat k větším úrovním podrobností postupně upřesnění nebo coarsenings.

Vzhledem k algoritmické a matematické povaze těchto tří konceptů lze ASM modely a jejich vlastnosti zájmu analyzovat pomocí jakékoli přísné formy ověření (zdůvodněním) nebo validace (experimentováním, testováním provedení modelu).

Dějiny

Koncept ASM je způsoben Jurij Gurevič, který to poprvé navrhl v polovině 80. let jako způsob, jak si vylepšit Turingova práce že každý algoritmus je simulované příslušným Turingův stroj. Formuloval ASM práce: každý algoritmus, jakkoli abstraktní, je krok za krokem emulovaný příslušným ASM. V roce 2000 Gurevič axiomatizovaný pojem sekvenčních algoritmů a prokázal pro ně práci ASM. Zhruba řečeno, axiomy jsou následující: stavy jsou struktury, přechod státu zahrnuje jen ohraničenou část státu a všechno je neměnný pod izomorfismy struktur. (Struktury lze zobrazit jako algebry, což vysvětluje původní název vyvíjející se algebry Pro ASM.) Axiomatizace a charakterizace sekvenčních algoritmů byly rozšířeny na paralelní a interaktivní algoritmy.

V 90. letech byla pomocí komunitního úsilí vyvinuta metoda ASM s využitím ASM pro formální specifikace a analýza (ověřování a validace ) z počítačový hardware a software. Komplexní specifikace ASM programovací jazyky (počítaje v to Prolog, C, a Jáva ) a designové jazyky (UML a SDL ) byly vyvinuty. Podrobný historický účet lze nalézt v AsmBook (Kapitola 9) nebo vtento článek.

K dispozici je řada softwarových nástrojů pro provádění a analýzu ASM.

Publikace

Knihy

Behaviorální modely pro průmyslové standardy

Nástroje

(v historickém pořadí od roku 2000)

Reference

  • Y. Gurevič, Evolving Algebras 1993: Lipari Guide, E. Börger (ed.), Specifikace a metody ověřování, Oxford University Press, 1995, 9-36. (ISBN  0-19-853854-5)
  • E. Börger a R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003. (ISBN  3-540-00702-4)
  • R. Stärk, J. Schmid a E. Börger, Java a Java Virtual Machine: Definice, Ověření, Ověření, Springer-Verlag, 2001. (ISBN  3-540-42088-6)
  • Y. Gurevič, Sekvenční abstraktní stavové stroje zachycují sekvenční algoritmy, Transakce ACM ve výpočetní logice 1 (1) (červenec 2000), 77-111.

externí odkazy