ИСТИНА

В рамках проекта предполагается разработка методов и средств решения задачи верификации параметризованных моделей для класса реагирующих систем, удовлетворяющих следующим ограничениям: 1) в системе используется асинхронный параллелизм; 2) процессы взаимодействуют посредством передачи сообщений; 3) коммуникационная топология системы фиксируется для каждой системы и описывается регулярным образом; 4) процессы порождаются на основе заданного конечного множества прототипов; 5) процессы и каналы связи считаются надежными; 6) свойства реагирующей системы и моделей параметризованного семейства описываются при помощи логики линейного времени. В ходе выполнения проекта планируется решить следующие задачи: - разработать алгоритмы построения отношений симуляции с учетом симметричности проверяемых моделей; разработать алгоритмы построения контрпримеров, демонстрирующих нарушение требований симуляции; интегрировать разработанные алгоритмы в систему верификации параметризованных моделей. - провести экспериментальную проверку применимости разработанных алгоритмов; исследовать способы представления коммуникационной топологии и параметризованным системам, альтернативные сетевым грамматикам; - разработать итеративные алгоритмы поиска инвариантов с построением отношений симуляции и применением методов абстракции для заданных свойств; интегрировать разработанные алгоритмы в систему верификации параметризованных моделей.