Evgeny_CD, Архитектор (05.12.2011 11:58, просмотров: 131) ответил Д.ARMоед на Не, EventB - не матан. Это хорошо формализуемый слой системы проектирования, в котором нужно разделить состояния.
Не понял. Если граф перехода КА синзезирован в виде функции, и она синтезирована на С правильно (реентерабельная, работает только с локальными переменными, все, что передается ей - RO, она возврашает либо стандартно, либо в спецальную структуру, которую для верности проверяют) - то все это на ура откомпилится стандартными С тулчейнами и 100% будет работать.
Для верности добавить еще проверку времени - не просрали ли мы реальное время за счет всей абстракции - и будет супер-надежно. Т.е. мы собрали данны для автомата, и говорим - суперавтомат, давай, твори, но творить ты должен до времени Ч вот по этоу таймеру. На выходе из горы функций проверям - таймер заикспарился или нет.
Кроме вездесущего ZOG еще должно пройти время на вырашивание специалистов и создание технологии. От работ Булля до первого кампука времени утекло с полвека...