Abstrakt statsmaskin

Inom datavetenskap är en abstrakt tillståndsmaskin ( ASM ) en tillståndsmaskin som arbetar på tillstånd som är godtyckliga datastrukturer ( struktur i betydelsen matematisk logik , det vill säga en icke-tom uppsättning tillsammans med ett antal funktioner ( operationer ) och relationer över uppsättning).

Översikt

ASM -metoden är en praktisk och vetenskapligt välgrundad systemteknisk metod som överbryggar gapet mellan de två ändarna av systemutveckling:

den mänskliga förståelsen och formuleringen av verkliga problem ( krav fångas genom noggrann högnivåmodellering på den abstraktionsnivå som bestäms av den givna applikationsdomänen)
distributionen av deras algoritmiska lösningar genom att kodexekvera maskiner på föränderliga plattformar (definition av designbeslut, system- och implementeringsdetaljer).

Metoden bygger på tre grundläggande koncept:

ASM : en exakt form av pseudokod som generaliserar finita tillståndsmaskiner för att fungera över godtyckliga datastrukturer
markmodell : en rigorös form av ritningar, som fungerar som en auktoritativ referensmodell för designen
förfining : ett mest allmänt schema för stegvisa instansieringar av modellabstraktioner till konkreta systemelement, vilket ger kontrollerbara kopplingar mellan de mer och mer detaljerade beskrivningarna i de successiva stadierna av systemutveckling.

, exekverar en enskild agent ett program i en sekvens av steg, eventuellt interagerande med dess omgivning. Denna idé utvidgades till att fånga distribuerade beräkningar , där flera agenter kör sina program samtidigt.

Eftersom ASM modellerar algoritmer på godtyckliga abstraktionsnivåer, kan de ge vyer på hög nivå, låg nivå och mellannivå av en hårdvaru- eller mjukvarudesign. ASM-specifikationer består ofta av en serie ASM-modeller, som börjar med en abstrakt markmodell och fortsätter till högre detaljnivåer i successiva förfinningar eller förgrovningar.

På grund av den algoritmiska och matematiska karaktären hos dessa tre begrepp kan ASM-modeller och deras egenskaper av intresse analyseras med hjälp av vilken rigorös form av verifiering som helst (genom resonemang) eller validering (genom experiment, testning av modellexekveringar).

Historia

Konceptet med ASM beror på Yuri Gurevich , som först föreslog det i mitten av 1980-talet som ett sätt att förbättra Turings tes att varje algoritm simuleras av en lämplig Turing - maskin . Han formulerade ASM-uppsatsen : varje algoritm, oavsett hur abstrakt den är, emuleras steg-för-steg av en lämplig ASM. År 2000 axiomatiserade Gurevich begreppet sekventiella algoritmer och bevisade ASM-avhandlingen för dem. Grovt uttryckt är axiomen följande: tillstånd är strukturer, tillståndsövergången involverar endast en avgränsad del av tillståndet, och allt är oföränderligt under isomorfismer av strukturer. (Strukturer kan ses som algebror , vilket förklarar det ursprungliga namnet utvecklande algebror för ASM.) Axiomatiseringen och karakteriseringen av sekventiella algoritmer har utvidgats till parallella och interaktiva algoritmer.

På 1990-talet utvecklades ASM-metoden, genom en gemenskapsinsats, med användning av ASM för den formella specifikationen och analysen ( verifiering och validering) av hårdvara och mjukvara . Omfattande ASM-specifikationer för programmeringsspråk (inklusive Prolog , C och Java ) och designspråk ( UML och SDL ) har utvecklats.

En detaljerad historisk redogörelse finns på annat håll.

Ett antal mjukvaruverktyg för exekvering och analys av ASM finns tillgängliga.

Publikationer

Böcker

AsmBook: Egon Börger , Robert Stärk. Abstrakta tillståndsmaskiner: En metod för systemdesign och analys på hög nivå
JBook: R.Stärk, J.Schmid, E.Börger. Java och Java Virtual Machine: definition, verifiering, validering
Proceedings/Journal Issues (sedan 2000)
- 2008: Springer LNCS 5238 Abstract State Machines, B och Z
- 2007: J.UCS specialnummer med utvalda papper från ASM'07
- 2006: Springer LNCS 5115 Rigorous Methods for Software Construction and Analysis , ASM och B Dagstuhl Seminarium
- 2005: Fundamenta Informatica Special Issue with Selected Papers from ASM'05 ( elektroniska handlingar )
- 2004: Springer LNCS 3052 Abstract State Machines 2004
- 2003: Springer LNCS 2589 Abstract State Machines 2003: Advances in Theory and Practice
- 2003: TCS specialnummer med utvalda papper från ASM'03
- 2002: Dagstuhl Seminar Report Teori och tillämpningar av abstrakta tillståndsmaskiner
- 2001: J.UCS 7.11 Specialutgåva med utvalda papper från ASM'01
- 2000: Springer LNCS 1912 abstrakta tillståndsmaskiner: teori och tillämpningar
Jämförande fallstudier med ASM-bidrag

Beteendemodeller för industriella standarder

OMG för BPMN (version 2006): Springer LNCS 5316
OASIS för BPEL: IJBPMI 1.4 (2006)
ECMA för C#: "A high-level modular definition of the semantics of C♯" doi : 10.1016/j.tcs.2004.11.008
ITU-T för SDL-2000: formell semantik för SDL-2000 och formell definition av SDL-2000 - Sammanställning och körning av SDL-specifikationer som ASM-modeller
IEEE för VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formell definition av en abstrakt VHDL'93 Simulator av EA-Machines. I: Carlos Delgado Kloos och Peter T.~Breuer (Eds.), Formal Semantics for VHDL , s. 107–139, Kluwer Academic Publishers, 1995
ISO för Prolog: "En matematisk definition av fullständig Prolog" doi : 10.1016/0167-6423(95)00006-E

Verktyg

(i historisk ordning sedan 2000)

ASMETA, Abstract State Machine Metamodel och dess verktygsuppsättning på SourceForge
AsmL
CoreASM , tillgänglig på CoreASM, en utbyggbar ASM-exekveringsmotor
AsmGofer på Archive.org
XASM open source-projektet på SourceForge

Bibliografi

Y. Gurevich, Evolving Algebras 1993: Lipari Guide , E. Börger (red.), Specification and Validation Methods , Oxford University Press , 1995, 9-36. ( ISBN 0-19-853854-5 )
Y. Gurevich, Sequential Abstract State Machines capture Sequential Algorithms , ACM Transactions on Computational Logic 1(1) (juli 2000), 77–111.
R. Stärk, J. Schmid och E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation , Springer-Verlag , 2001. ( ISBN 3-540-42088-6 )
E. Börger och R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis , Springer-Verlag , 2003. ( ISBN 3-540-00702-4 )
E. Börger och A. Raschke, Modeling Companion for Software Practitioners , Springer-Verlag , 2018. ( ISBN 978-3-662-56639-8 , doi : 10.1007/978-3-662-56641-1 )

externa länkar