Методы и технологии конструирования эффективных и надежных программ и программных систем на основе графовых моделей и семантических преобразований

Объектами исследования и разработки являются проблемы повышение эффективности и надежности компьютерного решения прикладных задач за счет совершенствования программного обеспечения перспективных вычислительных систем, разработка методов и средств функционального и логического программирования для поддержки супервычислений в рамках современных технологий, связанных с развитием телекоммуникационных сетей и центров коллективного пользования (ЦКП). Целью данной работы является развитие теории, методов и технологий оптимизирующей трансляции и конструирования эффективного, надежного, переносимого и адаптивного программного обеспечения для суперкомпьютеров и компьютерных сетей. Цель проекта - повышение эффективности и надежности компьютерного решения прикладных задач за счет совершенствования программного обеспечения перспективных вычислительных систем. Методы проведения работы: теоретико-графовые методы, методы трансформационного и объектно-ориентированного программирования, методы аннотирования программ, функциональных и логических спецификаций, специализации и визуальной обработки. Результаты работы: в процессе выполнения первого этапа работы были достигнуты все поставленные на этот этап цели проекта и получены следующие основные результаты: 1. Разработаны новые методы и эффективные алгоритмы анализа и визуализации сложно организованной информации большого объема на основе атрибутированной иерархической графовой модели с портами. Создана начальная версия системы визуализации Visual Graph, пригодная для научного и учебного применения. Помимо существенного развития реализованных в системе методов и алгоритмов визуализации информации на основе графовых моделей и анализа ее структурных свойств, новая версия системы поддерживает улучшенные возможности по работе с графовыми изображениями, более удобный пользовательский интерфейс и расширенные возможности импорта и экспорта графов. Разработаны методы и программные средства, поддерживающие конструирование и визуальную отладку Cloud Sisal программ, представленных в виде их графового внутреннего представления на языке GraphML. 2. На базисе языка спецификаций Event-B построен новый язык автоматного программирования. Тем самым в автоматном программировании появились средства верификации Event-B и возможность использования метода уточнения, а система Event-B стала поддерживать методы построения автоматных программ в дополнении к методу уточнения. Интеграция автоматного программирования с Event-B имеет особую важность для разработки программ критической инфраструктуры с повышенными требованиями к надежности и информационной безопасности. В соответствии с Российскими стандартами для сертификации таких программ требуется их формальная верификация в таких системах, как Event-B. Для разработки и формальной верификации автоматных программ не требуется других инструментов, кроме хорошо известной и доступной платформы Rodin, реализующей Event-B.