автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.06, диссертация на тему:Логические средства объектно-ориентированной технологии разработки и сопровождения программного обеспечения автоматизированных систем

На правах рукописи

КОКУШКИН ВЛАДИМИР АНАТОЛЬЕВИЧ

ЛОГИЧЕСКИЕ СРЕДСТВА ОБЪЕКТНО-ОРИЕНТИРОВАННОЙ ТЕХНОЛОГИИ РАЗРАБОТКИ И СОПРОВОЖДЕНИЯ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ АВТОМАТИЗИРОВАННЫХ СИСТЕМ

Специальность: 05.13.06. Авкэматизированные системы

управления

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата технических наук

МОСКВА - 1998

Работа выполнена в Московском институте пожарной безопасности МВД России

Научный руководитель: доктор технических наук,

профессор, академик РАЕН ТОПОЛЬСКИЙ Н.Г.

Официальные оппоненты: доктор технических наук,

профессор, академик МАИ ДЕЕВ В.В.

кандидат технических наук, С.//.С.

ЮРЧИК П.Ф.

Ведущая организация: Российский НИИ

информационных технологий и систем автоматизированного проектирования

Защита состоится " 7" 07 1998 года в 15 часов на заседании диссертационного совета Д 052.03.02 в Московском институте пожарной безопасности МВД России по адресу: 129366, Москва, ул.Б.Галушкина, д.4, в зале Совета.

С диссертацией можно ознакомиться в библиотеке МИПБ МВД России.

Автореферат разослан "X" ОК 1998 г., исх. № 7/7/.

Отзывы на автореферат с заверенной подписью и печатью просим направлять в МИПБ МВД России по указанному адресу.

Телефон для справок: 283-19-05.

Ученый секретарь

диссертационного совета

кандидат технических наук Т.Г.МЕРКУШКИНА

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

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

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

Учитывая вышеизложенное, в настоящей работе в качестве объекта исследования выбраны методы объектно-ориентированной технологии реализации жизненного цикла ПО (под методом в работе понимается совокупность языка моделирования, используемого для представления результатов разработки, и процессуальной части, состоящей из инструкций в отношении предпринимаемых шагов).

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

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

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

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

позволяет выбрать в качестве предмета исследования логические средства объектно-ориентированной технологии реализации жизненного цикла ПО автоматизированных систем.

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

Для достижения поставленной цели в работе были сформулированы и решены следующие задачи:

- проанализировать предпосылки и разработать схему жизненного цикла ПО автоматизированных систем для внедрения логических средств в объектно-ориентированную технологию;

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

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

- подтвердить выразительную мощность систем линейной логики и единого секвенциального исчисления на решении актуальных задач объектно-ориентированной технологии: моделирования параллельных взаимодействий и иерархического наследования с исключениями;

- разработать в качестве базы для автоматизации процессов объектно-ориентированной технологии реализации жизненного цикла ПО резолюционный метод поиска логического вывода в коммутативной классической линейной логике;

- продемонстрировать возможность построения языка абстрактного логического программирования на базе единого секвенциального исчисления для использования на этапе абстрактной спецификации.

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

Научная новизна работы заключается в следующем:

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

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

- на основе аппарата линейной логики решены задачи объектно-ориентированной технологии: моделирования параллельных взаимодействий и иерархического наследования с исключениями;

-построена процедура резолюционного поиска вывода для коммутативной классической линейной логики, доказана ее корректность и полнота;

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

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

Практическая реализация результатов исследования.

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

Унификация языков моделирования и применение элементов автоматизации на базе предложенных в работе подходов использованы при объектно-ориентированной разработке, сопровождении и модификации ПО, внедренного в практику работы специалистов военизированной охраны 12 дорог МПС РФ.

Результаты исследований внедрены и используются при чтении лекций по ряду курсов и при выполнении курсовых и дипломных проектов на кафедре АСУ МАДИ(ТУ).

Внедрение результатов работы подтверждено актами ВНИИПО МВД России, УВО МПС РФ и МАДИ(ТУ).

Публикации. В процессе работы над диссертацией опубликованы 32 печатные работы, результаты исследований нашли отражение в 9 рукописных трудах (отчеты и обзоры по НИР).

Апробация работы. Полученные результаты доложены на заседаниях и семинарах учебно-научного комплекса АСИТ МИПБ МВД России (1996-1998 гг.), кафедры АСУ МГТУ им. Н.Э.Баумана и кафедры АСУ МАДИ (1985-1996 гг.); на двух международных форумах "Технологии безопасности" (1997 и 1998 гг.); на четырех международных конференциях: "Ergonomics in Russia, the other independent States, and around the World" (1993 г.), "Информатизация систем безопасности" (1996г.), "Системы безопасности" (1997 г.), "Информатизация правоохранительных систем" (1997 г.), на семи всесоюзных и всероссийских конференциях и симпозиумах (19861997 гг.); на трех межрегиональных семинарах (1988-1992 гг.), на восьми научно-технических и научно-практических конференциях и семинарах (1982-1997 гг.).

На защиту выносятся:

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

ориентированной технологии, основные требования к компонентам схемы и структуре их взаимодействия;

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

- процедуры решения задач объектно-ориентированной разработки ПО на основе аппарата линейной логики: моделирование параллельных взаимодействий и иерархического наследования с исключениями;

- методовы поиска выводов в исчислениях линейной логики для автоматизации решения задач объектно-ориентированной технологии разработки ПО;

-методы резолюции для поиска вывода в коммутативной классической линейной логике;

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

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и четырех приложений. Общий объем диссертации составляет /8 8" страниц, в том числе 36 рисунков, ■? таблиц и списка литературы из 191 наименования.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

чертой индустриально организованного ПО является его большая сложность, и детально проанализированы ее причины.

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

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

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

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

В качестве оснований, наиболее подходящих для единообразного решения затронутых выше проблем, выбран

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

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

Во главе 2 "Исследование семантических и операциональных свойств логических систем для формализации и автоматизации объектно-ориентированной технологии" продемонстрировано место логического вывода в области информационных технологий, проанализированы существующие синтаксические представления и семантические интерпретации, на их основе разработана схема классификации правил вывода в секвенциальных системах, которая позволила более четко выявить "ответственность" правила или их группы за обеспечение определенных свойств логических исчислений.

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

Традиционное исчисление классической логики ЬК не обладает ни одним из этих свойств, а интуиционистское исчисление Ь,1 - только первым. Таким образом, объектно-

Физический проект

Рис. Схема жизненного цикла ПО для использования логических средств в объектно-ориентированной технологии

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

Анализ перечисленных свойств с использованием схемы классификации правил позволил связать достаточно большую их часть со структурной группой правил: ослаблением (W), сокращением (С) и перестановкой (Е). "Хорошими" комбинациями этих правил являются C+W+E, W+E, Е и 0, которым соответствует классическая, аффинная, коммутативная линейная и некоммутативная линейная классические логики. Удаление правил (W) и (С) приводит к расщеплению группы классических логических связок на мультипликативную группу и аддитивную группу линейных связок и появление линейной импликации, которая носит причинный характер. Удаление правила (Е) ведет к дальнейшему расщеплению отрицания и импликации на пост- и ретросвязки.

Показано, что в отсутствие правил (W) и (С) одновременное использование правил для мультипликативной импликации и аддитивной импликации приводит к системе, удовлетворяющей свойству элиминации сечения (Cut) и эквивалентной коммутативной классической линейной пропозициональной логике. Данное свойство позволило получить основные эквивалентности для линейных связок и констант и подтвердить тем самым наличие большинства семантических свойств, сформулированных в приведенных выше требованиях к перспективной логической системе.

Полное отсутствие правил (W) и (С) существенно ограничивает выразительную мощность системы, поэтому в работе используются модальные связки, которые позволяют применять правила (W) и (С) только к предваренным ими формулам.

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

Полученное подобным образом единое секвенциальное исчисление LU объединяет с помощью единообразной организации

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

В главе 3 "Разработка логических моделей параллельных взаимодействий и иерархического наследования с исключениями" демонстрируется выразительная мощность и естественность линейнологических решений для достаточно разнородных задач объектно-ориентированной технологии реализации жизненного цикла ПО автоматизированных систем.

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

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

На основании указанных аналогий в работе построен метаязык, позволяющий описывать известные модели параллельных взаимодействий с помощью правил для линейных связок. В качестве модели-примера выбрана модель действующих объектов (actors).

В этом случае мультипликативная конъюнкция расс-

матривается как оператор параллельной композиции с правилом

Г, А, В I—Д

—- (®L),

Г, А ® В Ь-Д

где ресурс А®В расщепляется на ресурсы А и В в контексте Г при обратной дедукции, а правила для аддитивной конъюнкции

рассматриваются как выбор той компоненты из А&В, которая верифицирует А&В в контексте Г. Локальные переменные вводятся с помощью правил квантификаци, создание копий формул и хранение их в памяти моделируется с помощью правил сокращения (СЬ) и дереликции (БЬ):

Г, !А, А I—А Г, !А, !А I—А Г, !А НД

(ОЬ) (СЬ),

а процесс синхронизации моделируется на основе правил для мультипликативной импликации.

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

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

Идея моделирования таксономических выводов с помощью линейной дедукции выглядит следующим образом. Предположим, что В, С, Б, И., Б, и - атомарные символы базовых предикатов, эквивалентных узлам ТСИ. Сформулируем связанные с ними аксиомы таким образом, чтобы единственными выводимыми импликациями, соответствующими ребрам ТСИ, были бы "Б влечет С и и и В" и "Б влечет Э и Я и не и". В качестве и используем

мультипликативную конъюнкцию заменяем С на 1 &С, и на 1&С и В на 1&В в "О влечет С и и и В", а "не и" на II—о1 в "Б влечет О и II и не и". Аксиомами в нашем случае будут:

Б Н (1 & С) О (1 & и) ® (1 & В) и

Б К- (1 & Б) <8> (1 & Я) О (и—о 1). Показано, что линейная дедукция позволяет получать из этих аксиом необходимые таксономические утверждения, которые демонстрирует иерархическое наследование по умолчанию С и В из Э с одновременной блокировкой ссылки на и.

Эта идея позволила определить для ТСИ язык линейной логики, включающий связки —о, ! и константу 1,

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

Как и в случае предыдущей задачи переход к единому секвенциальному исчислению ЫГ позволяет использовать решения, основанные на линейных моделях классических и интуиционистских связок.

В главе 4 "Разработка методов поиска вывода для исчислений линейной логики" строится база для автоматизации решения задач объектно-ориентированной технологии. Показано, что если получено некоторое представление задачи в виде секвенции в логическом исчислении, то мы можем использовать для ее решения теорию поиска вывода. Наиболее естественным методом является поиск "снизу-вверх", в ходе которого строится дерево поиска вывода, которое превращается в дерево вывода, когда все его листья оказываются аксиомами исчисления. Проанализированы проблемы, возникающие при подобном поиске, и методы их преодоления с помощью элиминации сечений, введения метапеременных и перехода к локальному принципу обработки информации на основе алгоритма унификации. Дана

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

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

На основе взаимного моделирования правил вывода для И и Рр построена новая резолюционная система Ксох Для линейного клаузального представления с помощью определяющих аксиом. Доказана теорема о корректности пропозициональной части Исах-

Для доказательства полноты правил Ксох (пропозициональный случай) разработано преобразование вЯ деревьев вывода из всах в Исах и доказана следующая теорема. Пусть с! - свободный от сечений вывод пропозициональной формулы Б в Осах : I— Б), а < АХр, Рр > - клаузальная форма для Б. Тогда ОЯ(<1): I— ахр Рр является выводом Ь дхр Рр в ЯРсох- □

С помощью метода Замова рассмотренные результаты распространены на случай кванторов, т.е. на все исчисление 11сах-

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

следовательно, производить погружение тактик вывода из вссьь в Ксси. •

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

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

Для этого линейные связки делятся на "асинхронные" и "синхронные", вводится фокусирующая процедура вывода, которая превращает синхронную последовательность связок в критический (непрерывный) процесс.

Подобная процедура поиска является унифицированным доказательством и позволяет операционально отражать манипуляцию ресурсами, параллелизм и синхронизацию, а также строить метапредставления для классических и интуиционистских фрагментов. Эти свойства ЫГ делают его перспективным языком для абстрактной спецификации в объектно-ориентированной технологии.

ОСНОВНЫЕ ВЫВОДЫ

В работе получены следующие основные теоретические и практические результаты.

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

2. Разработана схема жизненного цикла ПО автоматизированных систем для внедрения логических средств в объектно-ориентированную технологию.

3. В результате семантических и операциональных исследований логических систем с точки зрения соответствия задачам объектно-ориентированной технологии выявлен их нетрадиционный характер.

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

5. Решены на базе линейной логики и единого секвенциального исчисления актуальные задачи объектно-ориентированной технологии: моделирования параллельных взаимодействий и иерархического наследования с исключениями.

6. Продемонстрирована возможность автоматизации процессов объектно-ориентированной технологии на основе методов поиска логических выводов.

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

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

9. Предложенная схема жизненного цикла и логические средства использованы при создании и сопровождении ПО автоматизированных рабочих мест (АРМ) для специалистов, осуществляющих функции Государственного пожарного надзора; указанные АРМы внедрены и эксплуатируются в большинстве территориальных органов управления и подразделениях ГПС МВД России.

10. Предложенные в работе подходы для унификации языков моделирования и применения элементов автоматизации использованы при объектно-ориентированной разработке, сопровождении и модернизации ПО автоматизированных систем,

внедренных в практику работы специалистов военизированной охраны 12 дорог МПС РФ.

11. Результаты исследований внедрены и используются при чтении лекций по ряду курсов и при выполнении курсовых и дипломатических проектов на кафедре АСУ МАДИ(ТУ).

Основные положения диссертационного исследования опубликованы в следующих работах.

1.Будихин A.B., Кокушкин В. А., Самохвалов Э.Н. Автоматизация концептуального проектирования систем баз данных в АСУ // Кибернетика и исследование операций в управлении учебным процессом: Тез. докл. межреспубликанского семинара, Рига, 14-19 мая 1984. - Рига: РПИ, 1984. - С. 193-194.

2. Кокушкин В.А., Самохвалов Э.Н. Использование логики первого порядка для решения задач реляционного проектирования баз данных//X Научн.-техн. конф.: Тез. докл., Москва,25-26 апреля 1984.-Москва; 1984.-С. 91.

3. Кокушкин В.А., Самохвалов Э.Н. Применение теории первого порядка для проектирования реляционных баз данных//Проектирование автоматизированных систем контроля и управления сложными объектами: Тез. докл. Всесоюзной школы молодых ученых, 16-21 октября, 1984, Туапсе. - Харьков: ХПИ, 1984.-С. 33.

4. Кокушкин В.А., Самохвалов Э.Н. Применение многосортного исчисления предикатов для проектирования ограничений целостности // Проблемы создания и применения диалоговых информационных систем в автоматизированных системах организационного управления, Материалы научн.-техн. конф., 11-14 сентября 1984, Таллин. Часть 2. - Таллин: Валгус, 1985. -С. 194-199.

5. Самохвалов Э.Н., Кокушкин В.А., Будихин A.B. Методы обновления информации в интеллектуальных базах данных //Проблемы автоматизации организационного управления: Тез. докл. Всесоюзной конф., 21-25 октября 1985. - Тбилиси, 1985. - С. 265-266.

6. Будихин A.B., Кокушкин В.А. Автоматизация проектирования интеллектуальных баз данных на основе логического программирования // Математические модели и вычислительная техника в управлении учебным процессом высшей школы: Тез. докл. межвузовского научн.-метод. семинара, 20-23 мая, 1986, Рига. Часть 1. - Рига: РПИ, 1986. - С. 126-127.

7. Будихин A.B., Кокушкин В.А. Автоматизация проектирования и сопровождения интеллектуальных баз данных на основе логического программирования // Эргономическое обеспечение и автоматизация проектирования и испытаний человеко-машинных систем: Материалы научн.-техн. семинара, Ленинград, 17-18 марта 1986, - Ленинград: ЛДНТП, 1986. - С. 34-38.

8. Будихин A.B., Кокушкин В.А. Формализация концептуальной модели данных одного класса// Эффективность, качество и надежность систем человек-техника: Тез. докл. VIII Всесоюзн. симп. Тбилиси, 28-30 сентября, 1987. - Тбилиси, 1987. -С. 19.

9. Будихин A.B., Кокушкин В.А., Кудрявцева М.Г. Методы ассимиляции знаний при построении АОС // Эффективность применения автоматизированных обучающих систем в учебном процессе высшей школы: Тез. докл. Всесоюзн. Научн.-метод. совещания, Рига, 2-4 марта, 1988. - Рига: РПИ, 1988. - С. 19-21.

10. Кокушкин В.А. Построение машины вывода для АОС //Методы и системы технической диагностики: Межвузовский научн. Сб. - Саратов: СГУ, 1988. - С. 81-82.

И. Кокушкин В.А. Использование метаданных в автоматизированных обучающих системах // Математические модели и вычислительная техника в управлении учебным процессом высшей школы: Тез. докл. межвузовского научн.-метод. семинара, Рига, 20-23 мая 1986. - Рига: РПИ, 1988. - С. 150-151.

12. Мешалкин Е.А., Кокушкин В.А., Дударев Г.И. Эксперные системы и перспективы их использования в пожарной охране: Обзор, информ. - М.: ГИЦ МВД СССР, 1988. - 43 с.

13. Брушлинский H.H., Кокушкин В.А. Методы обработки модальной информации // Системы баз данных и знаний: Тез. докл. IV Всесоюзн. конф.; Секция 1,- Калинин, 1989. - С. 10-11.

14. Будихин A.B., Кокушкин В.А. Объектно-ориентированный подход при проектировании баз знаний ИАСУ // Проблемы

развития АСУ и информационных услуг в новых условиях хозяйствования: Тез. докл. научн.-техн. конф.-Душанбе, 1989. - С. 16-17.

15.Будихин A.B., Кокушкин В.А., Погорнев В.М. Методы структурирования баз данных и баз знаний // Эргономика и эффективность систем человек-техника: Тез. докл. XV Межрегионального семинара, Игналина, 1989. - Вильнюс, 1989. - С. 72-73.

16. Кокушкин В.А., Будихин A.B., Бойко С.И. Использование дедуктивного вывода в экспертных системах // Методы и системы технической диагностики. Экспертные обучающие системы. Часть 1. - Саратов: СГУ, 1989. - С. 63-67.

17. Кокушкин В.А., Губарь А.М., Бойко С.И. Метод разработки баз данных и знаний в АСУ // Методология создания и опыт эксплуатации АСУ в гражданской авиации: Тез. докл. Всесоюзн. научн.-техн. конф., Рига, 13-15 ноября 1989. - Рига: ЦНИИ АСУ ГА, 1989. - Р. 207-208.

18. Мешалкин Е.А., Кокушкин В.А., Дударев Г.И. Системы поддержки решений и перспективы их использования в пожарной охране: Обзор, информ. - М.: ГИЦМВД СССР, 1989. - 39 с.

19. Кокушкин В.А. Программирование, ориентированное на обработку знаний // Эргономика и эффективность систем "Человек-техника": Тез. докл. XVI Межрегионального семинара, Игналина, 1990. - Вильнюс, 1990. - С. 78-82.

20. Кокушкин В.А., Бойко С.И., Баранов М.Д. Возможности гипертекстовой технологии для автоматизации нормативно-технической деятельности // Информационные технологии в пожарной охране: Сб. научн. тр. - М.: ВНИИПО МВД СССР, 1991. -С. 33-39.

21. Кокушкин В.А. Автоматизация процессов сопровождения баз знаний экспертных систем // Эргономика и эффективность систем человек-техника: Тез. докл. XVII Межрегионального семинара, Игналина, 3-7 июня, 1991 г. - Игналина, 1991. - С. 99.

22. Тадеуш C.B., Кокушкин В.А., Былинкин М.В., Власов В.П. Обоснование направлений автоматизации учета требований пожарной безопасности в нормах и правилах//Информационные технологии в пожарной охране: Сб. научн. тр.. - М.: ВНИИПО МВД СССР, 1991.-С. 23-29.

23. Кокушкин В.А., Баранов М.Д., Тадеуш C.B. Гипертекстовая модель для представления требований пожарной безопасности, содержащихся в СНиП // Организационно-технические проблемы пожарной охраны: Сб. науч. тр. - М.: ВНИИПО МВД РФ, 1992. - С. 27-32.

24. Кокушкин В.А. Формальные основы индустриальной технологии разработки программных систем (Расширенный реферат) // Эргономика в России, СНГ и мире: Опыт и перспективы: Международн. конф, СПб, 21-24 июня, 1993. - СПб, 1993. - С. 31-33.

25. Кокушкин В.А., Голома К.В., Шпак Н.М. Новая информационная технология для автоматизации нормативно-технической деятельности // Научно-техническое обеспечение противопожарных и аварийно-спасательных работ: Материалы XII Всероссийской научн.-практ. конф. - Москва, 1993. - С. 45-47.

26. Кокушкин В.А., Шлепнев М.М., Горбацков Ю.В. Автоматизация обработки информации о деятельности ГПН // Научно-техническое обеспечение противопожарных и аварийно-спасательных работ: Материалы XII Всероссийской научн.-практ. конф. - Москва, 1993. - С. 53-54.

27. Тадеуш C.B., Кокушкин В.А. Новое программное средство по определению категорий помещений и зданий по взрывопожарной и пожарной опасности "PETROL" // Пожарная безопасность, информатика и техника. - 1993. - № 1(3). - С. 79-82.

28. Кокушкин В.А., Тадеуш C.B., Бойко С.И., Петрова О.В. Структура программного комплекса по правилам пожарной безопасности//Пожарная безопасность 95: XIII Всероссийская научн.-практ. конф. Москва, 1995. - С.

29. Топольский Н.Г., Кокушкин В.А. Логическое объектно-ориентированное проектирование программного обеспечения автоматизированных систем безопасности // Информатизация систем безопасности (ИСБ-96): Материалы 5-ой Международн. конф., Москва, 30 октября 1996.-М.: МИПБ, 1996. - С. 25-26.

30. Топольский Н.Г., Кокушкин В.А. Новые информационные технологии для служб и администрации крупных городов //Безопасность больших городов:, Тез. докл. научн.-практ. конф., Москва, 1997- М., 1997. - Р. 185.

31. Топольский Н.Г., Кокушкин В.А., Мосягин А.Б. Основные преимущества Intranet-технологии для информационного обеспе-

чения ГПС II Информатизация правоохранительных систем: Тез. докл. МФИ-97, Москва, 2-3 июля 1997, Часть 3. - Москва: Академия управления МВД России, 1997.-С. 109-111.

32. Kokushkin W.A. Formal basic of industrial technology of program systems development (Extended abstract) // Ergonomics in Russia, the Other Independent states, and Around the World: Past, Present and Future: Proc. Scientific Conference, St. Petersburg, Russia, June 21-24, 1993. - P. C-21 - C-23.

Соискатель

МИПБ МВД России. Тир. 75 экз. Зак N Ъ5