Описано цикл робіт щодо реалізації ініційованої В. М. Глушковим ще у 60-х рр. програми "Алгоритм Очевидності", які плануються з точки зору нового рівня розуміння та у відповідності до нових тенденцій у галузі інформаційних технологій і комп'ютерних наук.

Математичне середовище - це система засобів, які підтримують інтерактивне маніпулювання знаннями, поданими у вигляді (формалізованих) математичних текстів. Теоретичним обгрунтуванням цього проекту є теорія взаємодії агентів та середовищ. Теорія реалізується на базі симулятора мови дій, розробленого в системі алгебричного програмування.

Изложены парадигмы и идеи академика В.М.Глушкова. Проанализировано современное состояние кибернетики и информационных технологий. Описаны новые идеи, компьютерные свойства новых объектов. Рассмотрены безбумажная информатика как новый этап взаимодействия человека с компьютерной средой, вопросы повышения внутреннего интеллекта ЭВМ как средство их совершенствования.

Розглянуто алгебричну специфікацію нової переписувальної машини для швидкого переписування термів. Доведено теореми щодо коректності специфікації. Запропоновано метод оптимізації стратегії ітеративного переписування.

Запропоновано підхід до перевірки потреб або специфікацій програмних систем. Сформульовано мову формальних потреб і властивості програм, що перевіряються. Розглянуто схему доведень деяких важливих динамічних властивостей.

Висвітлено теоретичні основи формалізації та верифікації вимог за допомогою базових протоколів, що використовують поняття атрибутної транзиційної системи. Описано аспекти реалізації системи VRS і статистичні результати використання цих засобів у деяких великомасштабних промислових розробках.

Рассмотрена проблема представления требований к поведению интерактивной системы в виде формальных спецификаций, а также ее верификация и генерация трасс, используемых для создания тестовых наборов. Исследован специальный класс спецификаций, представленный в виде базовых протоколов, в котором рассматриваются возможные виды противоречивости и неполноты. С помощью символьного моделирования требований, произведено порождение символьных трасс, используемых для тестирования создаваемой системы по различным критериям.

Розглянуто основні етапи становлення та розвитку теорії автоматів і її застосування до автоматизації проектування обчислювальних систем.

Приведены обзор достижений Института кибернетики им. В. М. Глушкова за 1992 - 2006 гг.; некоторые соображения, связанные с особой важностью информационных технологий; названы наиболее важные комплексные проблемы развития компьютерной области, в которые следует вкладывать наибольшие средства и концентрировать усилия науки и техники на их решении, имеющие прямое отношение к традициям и научному потенциалу Института кибернетики.

Індекс рубрикатора НБУВ: З973-018.021.1

Рубрики:

Комп'ютери та програмування

Шифр НБУВ: Ж14024 Пошук видання у каталогах НБУВ 

Описано програмні засоби паралельного пошуку логічного виводу у пропозиційному численні та надано результати експериментів з ними. Програмні засоби розроблено на базі системи алгебричного програмування АПС та кластерного комплексу СКІТ-1.

Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно з якою він обчислює найсильнішу постумову для символьних станів.

Представлен обзор современного состояния инсерционного моделирования - направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах.

Приведен обзор автоматических методов проверки правильности формальных моделей программных систем. Рассмотрены проверяемые свойства, методы редукции и современные инструментальные средства проверки моделей.

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

Описан новый генератор символьных трасс, разработанный для последней версии системы инсерционного моделирования. Основными характеристиками генератора являются использование графического представления описания многоуровневых моделей, разделение локальных описаний и отношения следования, возможность настройки на различные стратегии поиска, применение нового предикатного трансформера, допускающего кванторы общности с ослабленными ограничениями относительно предыдущих версий.

Рассмотрена новая модель кибер-физических систем, которая обобщает известные модели типа гибридных и временных автоматов. Обсуждены вопросы применения методов моделирования и верификации, накопленных в области программирования, к разработке кибер-физических систем.

Приведен ретроспективный анализ теории кибер-физических систем (КФС) и охарактеризовано ее современное состояние. Исследован ряд проблем, возникающих в теории гибридных автоматов. Рассмотрена полугрупповая система переходов, являющаяся основой распространения алгебраической теории взаимодействия размеченных транзиционных систем на КФС.

Получены результаты испытаний инструментов упрощения формул, а также описан алгоритм построения канонических форм линейных полуалгебраических формул (ЛПФ). Основным результатом работы является определение канонической формы ЛПФ, обладающей свойством единственности и другими полезными свойствами, а также описание алгоритма ее построения.

Показано, что в настоящее время безопасность и защищенность программных ресурсов является одной из наиболее актуальных проблем в ИТ-отрасли, поскольку действия злоумышленников становятся все более изощренными, а убытки от кибератак растут. Традиционные методы борьбы с кибератаками теряют свою эффективность, поэтому разработка новых методов и средств защиты программных ресурсов является насущной потребностью. Особенно интересными и перспективными являются разработки, базирующиеся на формальных методах с использованием современных алгебраических теорий.