| Целью работы является исследование и разработка формальных оснований автоматизации доказательства уточнения полных спецификаций требований спецификациями компонентов и их композиций в процессе интеграции множественных неоднородных источников данных и сервисов и композиционного проектирования информационных систем (ИС).
Разработанные методы и средства могут быть использованы как
часть инструментария эксперта-конструктора, осуществляющего композиционное проектирование ИС как в рамках локальных, так и в рамках распределенных библиотек компонентов.
При этом процесс проектирования ИС становится формально верифицируемым, что позволяет корректно использовать существующие компоненты, уменьшает время отладки и тестирования систем,
позволяет проектировать системы, надежность которых критична, и отказоустойчивые системы.
Разработанные методы ориентированы на использование при решении
разнообразных задач интеграции множественных неоднородных
информационных источников и сервисов:
-
синтез канонических моделей для
посредников над разнородными информационными источниками;
-
согласование
онтологий посредника и информационных источников;
-
поиск информационных
источников и сервисов, семантически релевантных заданным требованиям;
-
регистрация неоднородных информационных источников в предметных
посредниках;
-
генерация доказательно правильных адаптеров
информационных источников.
Результатами работы являются:
-
метод формального определения канонических информационных моделей, необходимых для
однородного представления разнообразных моделей представления информации,
используемых в неоднородных источниках;
-
метод отображения канонических информационных моделей в
теоретико-модельный формальный язык спецификаций, поддерживающий
уточнение (в качестве такого языка рассматривается Нотация абстрактных машин, AMN);
-
метод доказательства корректности
отображения информационных моделей с использованием
их денотационно-аксиоматической семантики;
-
инструментальное средство автоматического отображения
спецификаций ядра канонической модели в AMN
и методика использования этого средства совместно с
инструментальными средствами доказательства уточнения при решении
указанных практических задач проектирования ИС.
|
