За последние десятилетия накопилось большое количество
программных и информационных компонентов, которые были созданы
при разработке информационных технологий и автоматизированных
систем. Целью проекта СИНТЕЗ является
композиционное проектирование информационных систем (ИС). Для
достижения этой цели необходимо решить несколько задач. К ним
относятся разработка соответствующих теоретических методов и
реализация на ЭВМ автоматизированной системы построения ИС из
имеющихся готовых компонентов по заданным спецификациям. Большая
роль в современном проектировании отводится потокам работ
(workflow) как компонентам. Такие компоненты реализуют процессное
поведение.
Суть композиционного проектирования состоит в следующем.
Существует эксперт, снабженный набором инструментов,
автоматизирующих его работу. Эксперт имеет доступ к базе
метаинформации. В базе метаинформации содержатся спецификации
готовых программных компонентов на языке СИНТЕЗ. Этот
язык разрабатывался как средство унифицированного описания
разнородных компонентов. От других формальных языков спецификаций
его отличает большая выразительная сила. Эксперт формирует на
языке СИНТЕЗ спецификацию необходимой заказчику программной
системы (спецификацию требований). Затем, используя по
возможности вспомогательные инструменты, эксперт декомпозирует
спецификацию требований на части и для каждой такой части ищет в
базе метаинформации спецификацию, уточняющую ее. Если эта задача
выполнена успешно, то из программных компонентов, соответствующих
найденным уточняющим спецификациям, составляется система, которая
и возвращается заказчику в качестве ответа.
Центральным местом в процессе композиционного проектирования
является формальное доказательство факта, что одна спецификация
(спецификация компонента) уточняет другую (спецификацию
требований). Причем, в силу громоздкости необходимых для
доказательства действий, оно должно быть максимально
автоматизированным. Такое доказательство может быть проведено с
помощью некоторых специальных средств, например, B-технологии (B
Technology). Для B-технологии существует набор
инструментов, B-Toolkit, частично автоматизирующих
анализ спецификаций и доказательство факта уточнения. B-Toolkit
работает со спецификациями, представленными в нотации абстрактных
машин (Abstract Machine Notation, AMN).
Настоящая дипломная работа посвящена вопросам доказательства
факта уточнения для процессных компонентов. Для формального
описания таких компонентов язык СИНТЕЗ снабжен средствами
спецификации процессов --- процессной моделью, основой которой
служит процессная алгебра CSP (Communicating Sequential
Processes). Поскольку доказательство факта уточнения
реализуется средствами B, возникает задача отображения в AMN
процессной модели СИНТЕЗа, решению которой посвящена данная
дипломная работа. |
