VVB_ (18.05.2018 08:06, просмотров: 1) ответил VVB_ на Просветите немного, раз немного въехали в тему.Вот, например, инструмент Yakindu для реализации конечных автоматов на Си, с возможностью верификации выполнения программы уже в железе (или на ПК). Иногда пользуюсь. _https://www.itemis.com/en/yakindu/state-machine/documentation/user-guide/overview_what_are_yakindu_statechart_tools
Есть QP Framework. Я им не пользуюсь.
Это всё событийно-ориентированные инструменты моделирования.
Насколько я понял, SPIN & Co являются исследовательскими инструментами для учёных.
Эти инструменты имеют генератор кода из языка описания автоматов в другой язык (Java/C/C++). Уверен, что подобных генераторов много.
С моделями отличными от автоматов данные инструменты работать не могут -- не хватает языка. Тем не менее, можно почти всё закодировать в терминах конечных автоматов и произвести их верификацию, для этого и создан этот инструментарий.
Вроде бы у SPIN заявлено "прямое использование встраиваемого кода на Си" и некий "извлекать модели из Си в Promela", modex.
Что даёт применение SPIN к нашей практике, чего не могут дать более простые и понятные инструменты?