ВходНаше всё Теги codebook PARTS Поиск Опросы Закон Пятница
29 мая
/841681
Топик полностью
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 к нашей практике, чего не могут дать более простые и понятные инструменты?