Абстрактная государственная машина

В информатике абстрактный автомат состояний ( АСМ ) — это конечный автомат, работающий с состояниями , которые представляют собой произвольные структуры данных ( структура в смысле математической логики , то есть непустое множество вместе с рядом функций ( операций ) и отношений над набор).

Обзор [ править ]

Метод ASM — это практический и научно обоснованный метод системного проектирования , который устраняет разрыв между двумя сторонами разработки системы:

человеческое понимание и формулирование проблем реального мира ( фиксация требований посредством точного высокоуровневого моделирования на уровне абстракции, определяемом данной областью приложения)
внедрение своих алгоритмических решений машинами-исполнителями кода на меняющихся платформах (определение проектных решений, деталей системы и реализации).

В основе метода лежат три основные концепции:

ASM : точная форма псевдокода, обобщающая конечные автоматы для работы с произвольными структурами данных.
наземная модель : строгая форма чертежей, служащая авторитетной эталонной моделью для проектирования.
уточнение : наиболее общая схема поэтапного воплощения абстракций модели в конкретные элементы системы, обеспечивающая управляемые связи между все более подробными описаниями на последовательных этапах разработки системы.

В первоначальной концепции ASM один агент выполняет программу в виде последовательности шагов, возможно, взаимодействуя со своей средой. Это понятие было расширено для охвата распределенных вычислений , в которых несколько агентов одновременно выполняют свои программы.

Поскольку ASM моделируют алгоритмы на произвольных уровнях абстракции, они могут обеспечивать представления высокого, низкого и среднего уровня конструкции аппаратного или программного обеспечения. Спецификации ASM часто состоят из серии моделей ASM, начиная с абстрактной наземной модели и заканчивая более высокими уровнями детализации с последовательными уточнениями или уточнениями.

Благодаря алгоритмической и математической природе этих трех концепций, модели ASM и их интересующие свойства могут быть проанализированы с использованием любой строгой формы проверки (путем рассуждения) или проверки (путем экспериментирования, тестирования выполнения модели).

История [ править ]

Концепция ASM принадлежит Юрию Гуревичу способ улучшения тезиса Тьюринга о том, что каждый алгоритм моделируется , который впервые предложил ее в середине 1980-х годов как соответствующей машиной Тьюринга . Он сформулировал тезис ASM : каждый алгоритм, каким бы абстрактным он ни был , шаг за шагом эмулируется соответствующим ASM. В 2000 году Гуревич аксиоматизировал понятие последовательных алгоритмов и доказал для них тезис АСМ. Грубо говоря, аксиомы таковы:

Государства – это структуры,
затрагивает переход состояния только ограниченную часть состояния, и
все инвариантно относительно изоморфизмов структур. (Структуры можно рассматривать как алгебры , что объясняет оригинальное название «эволюционирующие алгебры» для ASM.)

Аксиоматизация и характеристика последовательных алгоритмов были распространены на параллельные и интерактивные алгоритмы.

В 1990-е годы благодаря общественным усилиям ^[1] был разработан метод ASM, использующий ASM для формальной спецификации и анализа ( верификации и валидации ) компьютерного оборудования и программного обеспечения . комплексные ASM-спецификации языков программирования (включая Prolog , C и Java ) и языков проектирования ( UML и SDL Разработаны ).

Подробный исторический отчет можно найти в другом месте. ^[2]^[3]

Доступен ряд программных инструментов для выполнения и анализа ASM.

Публикации [ править ]

Книги [ править ]

AsmBook: Эгон Бёргер , Роберт Старк. Абстрактные конечные автоматы: метод высокоуровневого проектирования и анализа систем
JBook: Р.Старк, Й.Шмид, Э.Бёргер. Java и виртуальная машина Java: определение, проверка, валидация
Труды/выпуски журнала (с 2000 г.)
- 2008: Springer LNCS 5238 Абстрактные конечные автоматы, B и Z
- 2007: Специальный выпуск J.UCS с избранными статьями ASM'07.
- 2006: Springer LNCS 5115 Строгие методы построения и анализа программного обеспечения , семинар ASM и B Dagstuhl
- 2005: Специальный выпуск Fundamenta Informatica с избранными статьями ASM'05 ( электронные материалы )
- 2004: Springer LNCS 3052 Абстрактные конечные автоматы 2004
- 2003: Springer LNCS 2589 Абстрактные конечные автоматы 2003: Достижения в теории и практике
- 2003: Специальный выпуск TCS с избранными статьями ASM'03.
- 2002: Отчет о семинаре Дагштуля «Теория и применение абстрактных государственных автоматов».
- 2001: Специальный выпуск J.UCS 7.11 с избранными статьями ASM'01.
- 2000: Springer LNCS 1912 Абстрактные конечные автоматы: теория и приложения
Сравнительные тематические исследования с участием ASM

модели для промышленных Поведенческие стандартов

OMG для BPMN (версия 2006): Springer LNCS 5316
ОАЗИС для BPEL: IJBPMI 1.4 (2006 г.)
ECMA для C#: «Модульное определение высокого уровня семантики C♯». дои : 10.1016/j.tcs.2004.11.008
ITU-T для SDL-2000: формальная семантика SDL-2000 и формальное определение SDL-2000 - Компиляция и выполнение спецификаций SDL как моделей ASM
IEEE для VHDL93: Э.Бёргер, У.Глессер, В.Мюллер. Формальное определение абстрактного симулятора VHDL'93 от EA-Machines. В: Карлос Дельгадо Клоос и Питер Т.~Бройер (ред.), Формальная семантика для VHDL , стр. 107–139, Kluwer Academic Publishers, 1995.
ISO для Пролога: «Математическое определение полного Пролога». два : 10.1016/0167-6423(95)00006-E

Инструменты [ править ]

(в историческом порядке с 2000 г.)

Библиография [ править ]

Ю. Гуревич, Развивающиеся алгебры, 1993: Руководство Липари , Э. Бёргер (редактор), Методы спецификации и проверки , Oxford University Press , 1995, 9-36. ( ISBN 0-19-853854-5 )
Ю. Гуревич, Последовательные абстрактные конечные автоматы захватывают последовательные алгоритмы , Транзакции ACM в вычислительной логике 1 (1) (июль 2000 г.), 77–111.
Р. Старк, Дж. Шмид и Э. Бёргер, Java и виртуальная машина Java: определение, проверка, валидация , Springer-Verlag , 2001. ( ISBN 3-540-42088-6 )
Э. Бёргер и Р. Штерк, Абстрактные конечные автоматы: метод проектирования и анализа систем высокого уровня , Springer-Verlag , 2003. ( ISBN 3-540-00702-4 )
Э. Бёргер и А. Рашке, помощник по моделированию для специалистов по программному обеспечению , Springer-Verlag , 2018. ^[4] ( ISBN 978-3-662-56639-8 , дои : 10.1007/978-3-662-56641-1 )

Ссылки [ править ]

^ Боуэн, Джонатан П. (2021). «Сообщества и предки, связанные с Эгоном Бёргером и ASM». В Рашке, Александр; Риккобене, Эльвиния; Шеве, Клаус-Дитер (ред.). Логика, вычисления и строгие методы: очерки, посвященные Эгону Бёргеру по случаю его 75-летия . Конспекты лекций по информатике . Том. 12750. Международное издательство Springer . стр. 96–120. дои : 10.1007/978-3-030-76020-5_6 . ISBN 978-3-030-76019-9 . S2CID 235414337 .
^ «Главная страница AsmBook» . Италия: Пизанский университет . Ноябрь 2005 года . Проверено 8 июня 2021 г. (Глава 9)
^ Бёргер, Эгон (2002). «Истоки и развитие метода ASM для проектирования и анализа систем высокого уровня» . Журнал универсальной информатики . 8 (1). doi : 10.3217/jucs-008-01-0002 .
^ Боуэн, Джонатан П. (ноябрь 2018 г.). «Эгон Бёргер и Александр Рашке: помощник по моделированию для специалистов по программному обеспечению». Формальные аспекты вычислений . 30 (6): 761–762. дои : 10.1007/s00165-018-0472-4 . S2CID 53086556 .

Внешние ссылки [ править ]

[bowen21-1] Боуэн, Джонатан П. (2021). «Сообщества и предки, связанные с Эгоном Бёргером и ASM». В Рашке, Александр; Риккобене, Эльвиния; Шеве, Клаус-Дитер (ред.). Логика, вычисления и строгие методы: очерки, посвященные Эгону Бёргеру по случаю его 75-летия . Конспекты лекций по информатике . Том. 12750. Международное издательство Springer . стр. 96–120. дои : 10.1007/978-3-030-76020-5_6 . ISBN 978-3-030-76019-9 . S2CID 235414337 .

[2] «Главная страница AsmBook» . Италия: Пизанский университет . Ноябрь 2005 года . Проверено 8 июня 2021 г. (Глава 9)

[3] Бёргер, Эгон (2002). «Истоки и развитие метода ASM для проектирования и анализа систем высокого уровня» . Журнал универсальной информатики . 8 (1). doi : 10.3217/jucs-008-01-0002 .

[4] Боуэн, Джонатан П. (ноябрь 2018 г.). «Эгон Бёргер и Александр Рашке: помощник по моделированию для специалистов по программному обеспечению». Формальные аспекты вычислений . 30 (6): 761–762. дои : 10.1007/s00165-018-0472-4 . S2CID 53086556 .

[1]

[2]

[3]

[4]