stringtranslate.com

Абстрактная машина состояний

В информатике абстрактный конечный автомат ( 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.

Публикации

Книги

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

Инструменты

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

Библиография

Ссылки

  1. ^ Боуэн, Джонатан П. (2021). «Сообщества и предки, связанные с Эгоном Бёргером и ASM». В Рашке, Александр; Риккобене, Эльвиния; Шеве, Клаус-Дитер (ред.). Логика, вычисления и строгие методы: эссе, посвященные Эгону Бёргеру по случаю его 75-летия . Конспект лекций по информатике . Том 12750. Springer International Publishing . С. 96–120. doi :10.1007/978-3-030-76020-5_6. ISBN 978-3-030-76019-9. S2CID  235414337.
  2. ^ "AsmBook Home Page". Италия: Университет Пизы . Ноябрь 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.

Внешние ссылки