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

В этой статье есть несколько проблем. Помогите улучшить ее или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалять эти сообщения ) В статье содержится список общих ссылок , но в ней отсутствуют соответствующие встроенные цитаты .Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Июнь 2021 г. ) (Learn how and when to remove this message) This article's use of external links may not follow Wikipedia's policies or guidelines. Please improve this article by removing excessive or inappropriate external links, and converting useful links where appropriate into footnote references. (June 2021) (Learn how and when to remove this message) (Learn how and when to remove this message)

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

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

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

Метод строится на трех основных концепциях:

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

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

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

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

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

• государства - это структуры,
• государственный переход затрагивает только ограниченную часть государства, и
• все инвариантно относительно изоморфизмов структур. (Структуры можно рассматривать как алгебры , что объясняет первоначальное название для 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
  • Управление паровым котлом: исследование спецификации, Springer LNCS 1165
  • Производственная ячейка: пример разработки программного обеспечения, модель ASM
  • Railcrossing: Формальные методы для вычислений в реальном времени, модель ASM
  • Управление освещением: пример инженерных требований, семинар в Дагштуле
  • Выставление счетов: пример сбора требований

• OMG для BPMN (версия 2006): Springer LNCS 5316
• OASIS для BPEL: IJBPMI 1.4 (2006)
• ECMA для C#: «Высокоуровневое модульное определение семантики C♯» doi :10.1016/j.tcs.2004.11.008
• ITU-T для SDL-2000: формальная семантика SDL-2000 и формальное определение SDL-2000 - Компиляция и запуск спецификаций SDL как моделей ASM
• IEEE для VHDL93: E.Boerger, U.Glaesser, W.Mueller. Формальное определение абстрактного симулятора VHDL'93 от EA-Machines. В: Carlos Delgado Kloos и Peter T.~Breuer (ред.), Formal Semantics for VHDL , стр. 107–139, Kluwer Academic Publishers, 1995
• ISO для Prolog: "Математическое определение полного Prolog" doi :10.1016/0167-6423(95)00006-E

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

• Верстак ASM
• ASMETA, метамодель абстрактной машины состояний и ее набор инструментов
• Асмл
• CoreASM , доступный на CoreASM, расширяемый механизм выполнения ASM
• AsmGofer на Archive.org
• Проект XASM с открытым исходным кодом на SourceForge

• Y. Gurevich, Evolving Algebras 1993: Lipari Guide , E. Börger (ред.), Specification and Validation Methods , Oxford University Press , 1995, 9-36. ( ISBN 0-19-853854-5 ) 
• Ю. Гуревич, Последовательные абстрактные машины состояний захватывают последовательные алгоритмы , ACM Transactions on Computational Logic 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 , doi : 10.1007/978-3-662-56641-1) 

• Абстрактные конечные автоматы
• AsmCenter Архивировано 2019-09-13 в Wayback Machine
• Набор инструментов TASM: спецификация, моделирование и формальная верификация систем реального времени