Козлов Илья Андреевич

С.185-195

С.196-208

Одним из путей решения этой проблемы является верификация моделей по методу Model Checking. Анализу подвергается модель многопоточной системы, представляющая собой ориентированный граф, рёбра которого отражают зависимости между потоками. В основе верифицирующего алгоритма для обнаружения взаимных блокировок лежит поиск сильно связных компонент (ССК) в этом графе. В статье изложен метод проверки целостности сильно связных компонент в рамках алгоритма поиска взаимных блокировок в многопоточных системах. Приведено краткое описание модели многопоточной системы и верифицирующего алгоритма. Описаны основные принципы подхода и приёмы, используемые для уменьшения вычислительной сложности.

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

В статье рассмотрены основные проблемы реляционных СУБД и причины того, что такие системы уже не могут удовлетворить всем современным требованиям. Описаны различные подходы к определению требований к транзакциям, а также основные методы масштабирования. Перечислены особенности нереляционных СУБД. Рассмотрены механизмы консистентного хеширования и управления конкурентным доступом с помощью многоверсионности.Приведена классификация нереляционных систем и рассмотрены особенности каждого класса.В заключительной части статьи описана иерархическая модель данных и рассмотрена СУБД IBM IMS, использующая эту модель. Проведен анализ перспектив использования нереляционных технологий в МГТУ им. Баумана.