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

Введение.

Глава 1. Модельно-технологический подход к применению формальных методов для повышения надежности проектирования. Основные принципы и идеи.

Введение. Качество проектирования и его связь с надежностью.

1.1. Основные принципы модельно-технологического подхода.

1.2. Общая модель технологии.

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

1 АТиповой комплекс массовых задач повышения надежности проектирования на основе формальных методов.

Подходы к решению и обеспечению.

1.5. Практические применения модельно-технологического подхода.

Результаты и выводы по главе 1.

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

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

Методы и средства решения.

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

2.2. Базовое семейство схем языков типа^^.

2.3. Семейство схем языков типа

2.4. Сравнение языков функций и их выразительных возможностей.

Результаты и выводы по главе 2.

Глава 3. Сверхмассовая задача анализа внешнего поведения структурированных объектов. Методы и средства решения.

3.1. Общий подход к решению частных массовых задач.

3.2. Базовая задача анализа внешнего поведения на основе локальных эквивалентных преобразований и ее ближайшие аналоги.

3.3. Бинарные программы и схемы выбора.

3.4. Сети связи.

3.5. Ленточные автоматы. Автономные автоматы.

3.6. Модель типа схем и ее возможности.

Результаты и выводы по главе 3.

Глава 4. Другие технологические задачи, связанные с контролем и обеспечением правильности.

4.1. Задачи проверки и обоснования правильности.

Общий подход.

4.2. Критерии правильности и их формализация.

4.3. Верификация и ее связь с анализом внешнего поведения. Верификационная отладка.

4.4. Технологическая задача оценочного тестирования.

4.5. Пример внедрения

Результаты и выводы по главе 4.

Глава 5. Новый математический аппарат анализа и верификации программ.

Введение. Нерешенные проблемы. Подходы к решению.

5.1. Языки типа Л'рЧ и их базовая алгебраическая система.

5.2. Языки типа Л*рТ1Ж и их базовая алгебраическая система.

5.3. Представление программ LTO-схемами.

5.4. Постановка задач анализа внешнего поведения и верификации.

5.5. Методы решения на основе эквивалентных преобразований LTO-схем.

Актуальность темы исследования. Хорошо известна проблема надежности программного обеспечения (ПО) и ее связь с проектными ошибками; известны связанные с этой проблемой затраты на создание и обслуживание ПО, в особенности - для приложений повышенной социальной или экономической значимости. Для программно-технических средств (ПТС) в составе вычислительных систем эта проблема также признается. Целесообразно рассматривать с единых научных позиций надежность технологий создания ПТС как возможность обеспечения таких показателей надежности ПТС как правильность, безошибочность, а также других критических свойств.

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

Это - направление формализованного проектирования, которое активно расширяет свои позиции на западе [127, 172, 43], и - в практическом плане - развивается сравнительно немногими известными отечественными учеными (В.Н. Агафонов [32-34], В.А. Непомнящий [72-75]), и организационное направление, наиболее последовательным и активным публичным пропагандистом которого в нашей стране является В.В. Липаев [63-65].

Подчеркнем, что эти два направления не только совместимы, но и могут выступать как взаимодополняющие. Достаточно сказать, что организационное направление нуждается в конкретных методах, тогда как направление формальных методов имеет целью создание таких методов. Совместимость подтверждается не только имеющимися практическими примерами применения формальных методов в жестко регулируемых областях [127, 43, 203], но и рекомендациями различных стандартов [например, 170].

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

1 Уточним, что термин "верификация" в настоящее время используется в двух смыслах. В одном, более широком смысле он означает комплекс строго регламентированных (и в этом смысле - формальных) процедур, применяемых на каждом этапе процесса разработки программного обеспечения для проверки соответствия продукта всем требованиям предыдущего этапа. При этом в одних случаях, например, по стандартам МЭК [170], верификация включает также тестирование, а в других - тестирование относится к демонстрации правильности. В более узком смысле, в котором этот термин используется в данной работе и который характерен для теоретических работ, верификация означает доказательство правильности. В последнем случае практики нередко говорят о формальной верификации, хотя степень формализации в практических подходах к верификации может значительно варьироваться, и наиболее значимой характеристикой здесь оказывается применение логико-математических методов обоснования правильности.

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

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

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

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

В развитие теоретических основ формальных методов вложили свой вклад крупнейшие ученые В.М.Глушков, А.А.Летичевский,

В.А.Непомнящий, В.В.Непейвода, В.Н.Агафонов,, Г.Е.Цейтлин, В.Н.Редько, С.Хоар, Р.Флойд, Х.Миллз, Э.Дейкстра, З.Манна, Д.Парнас, Дж.П. Боуэн, С.Герхарт, П.Зейв, Р. Гласс и многие другие. Имеются реальные успехи в использовании формальных методов в практических разработках для приложений с повышенными требованиями к надежности, и фирменные технологии, особенно известные за рубежом. Среди отечественных работ следует выделить разработку технологии ИКАР в ИПУ РАН под руководством A.A. Амбарцумяна для построения систем низовой автоматики для потенциально опасных объектов [37].

Однако несмотря на достигнутые успехи, общепризнано [127, 172, 43], что продвижение в практические технологии наукоемких формальных методов сегодня сталкивается с многочисленными трудностями.

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

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

2 Более точно было бы говорить о надежности проектирования и испытаний, однако мы рассматриваем испытания как составную часть процесса создания ПТС, предшествующую выдаче результатов завершенного проекта. На практике этот процесс обобщенно называют проектированием или разработкой (хотя при его разбиении на стадии, или этапы термины «проектирование», «разработка» часто относят к отдельным стадиям этого процесса). ции, ориентированные на практические применения формальных методов и 2) наш собственный опыт успехов и неудач на этом поприще. Выделены следующие группы проблем, которые оцениваются как наиболее серьезные [17]:

• проблема взаимного непонимания теоретиков и практиков;

• проблема участия человека при использовании формальных методов;

• разнообразие "мира программ" в сочетании с его открытостью;

• теоретические сложности и ограничения (в первую очередь, неадекватность имеющегося и используемого математического аппарата).

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

• проблема частичной корректности программ, по сути искусственная,

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

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

• узость алгебры структурированных программ, которая не охватывает неструктурированные программы с необязательно "плохой" структурой.

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

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

- технологического,

- теоретического,

- методологического.

Объектами исследования и разработки при таком комплексном подходе являются, с одной стороны, теоретические средства для повышения надежности проектирования посредством формальных методов, а с другой, - процессы человеческой деятельности по проектированию ПТС и созданию и/или адаптации научно-методического и языкового обеспечения (НМЯО) для конкретных технологий проектирования. При этом выделяются два уровня рассмотрения процессов: технологическая деятельность и интеллектуальные процессы проектирования и создания и/или адаптации НМЯО.

Основные задачи, решаемые в диссертации в соответствии с поставленной целью, таковы:

• анализ проблем, препятствующих продвижению формальных методов в практику;

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

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

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

• разработка и апробация техник порождения формализованных знаний, ориентированных на

- повышение корректности знаний при проектировании,

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

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

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

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

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

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

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

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

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

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

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

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

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

- ориентации предлагаемых математических средств на корректность;

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

Реализация результатов. Результаты и положения диссертации были использованы

- при разработке и применении технологии промежуточной верификации векторного процессора в составе вычислительного комплекса ПС-320 (ИПУ- НПО «Элва») - 1985 г.;

- в частной технологии верификации функциональных схем локальных алгоритмов управления АСУТП АЭС нижнего уровня в составе технологии для инструментального комплекса ИКАР3 и при проведении верификации отдельных алгоритмов - 1990 г.,

- в технологии подготовки и проведения сертификационных испытаний в Испытательной лаборатории, аккредитованной Госстандартом России, и в конкретных испытаниях по этой технологии,

- при разработке нормативно-технической документации по сертификации программных средств для атомной промышленности (заказчики: ФГУП «Атомэнергопроект», г.Москва - 1992 г., концерн «Росэнергоатом» - 1996г.);

- при создании программ обеспечения качества в проектах с участием концерна «Росэнергоатом» - 1997-1998 гг.;

- при выполнении комплекса работ по верификации проекта «Рабочее программное обеспечение и конфигуратор», выполняемого

3 Технология и инструментальный комплекс разрабатывались в ИПУ РАН под руководством А.А.Амбарцумяна. для АЭС «Бушер» (заказчик ФГУП «Атомэнергопроект», г. Москва) -2001 г.

Апробация работы. Основные научные результаты работы докладывались и обсуждались с 1986 г. на 3-х международных, ряде всесоюзных и российских конференций, совещаний, школ-семинаров по теории релейных систем и конечных автоматов, по технической кибернетике, технической диагностике, искусственному интеллекту, по проектированию динамических систем, по логическому моделированию, по синтезу, тестированию, верификации и отладки программ, по проблемам создания и использования мини- и микро-ЭВМ, по сертификации программного обеспечения, по параллельным вычислениям и задачам управления; на общемосковских семинарах по искусственному интеллекту, логическому моделированию, на научно-производственном семинаре НПТЦ им. Хруничева, на семинарах в Институте проблем управления РАН.

Публикации. По теме диссертации опубликована 31 научная работа, включая одну книгу « Поиск подходов к решению проблем» в соавторстве, в которой глава 3 и разд. 1.1, относящиеся к теме диссертации, написаны автором по результатам, полученным самостоятельно. Все результаты, представленные в диссертации, получены автором самостоятельно. Из работ, опубликованных в соавторстве, в диссертацию включены результаты, полученные автором лично.

Структура и объем работы. Диссертация состоит из введения, шести глав, заключения, списка литературы и приложения.

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

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

Выделенные проблемы, предопределили три плана исследований в направлении поставленной цели диссертации:

- технологический,

- теоретический,

- методологический.

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

Общий подход включает

1. проверенный на практике метод повышения надежности специализированных технологий на основе формальных методов,

2. совместимые теоретические идеи и подходы к решению типового комплекса технологических задач повышения надежности,

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

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

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

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

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

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

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

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

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

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

• Показано, как предложенные методы используются 1) для решения технологических задач типового комплекса, 2) в качестве методов организации и переноса знаний при создании научно-методического и языкового обеспечения новых частных задач повышения надежности.

230

Результаты диссертации применялись

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

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

Совокупность результатов, полученных по всем направлениям, позволяет сделать следующие выводы:

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

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

Для развития этого направления представляется целесообразным проведение междисциплинарных исследований с привлечением психологии мышления.

1. Абрамова H.A. Общий подход к анализу внешнего поведения объектов, представленных функциональными схемами, на основе эквивалентных преобразований. Часть 1. // Автоматика и телемеханика, 1993, №3, с. 115-134.

2. Абрамова Н.А Общий подход к анализу внешнего поведения объектов, представленных функциональными схемами, на основе эквивалентных преобразований. Часть 2. // Автоматика и телемеханика, №4, с.167-181

3. Абрамова H.A. Об одном подходе к построению языков функциональных спецификаций, ориентированном на корректность. // Автоматика и телемеханика, 1995, №2, с. 164-189.

4. Абрамова H.A. Анализ внешнего поведения бинарных программ и схем выбора на основе локальных эквивалентных преобразований. // Автоматика и телемеханика, 1995, №.6, с. 127-147.

5. Абрамова H.A. Метод анализа внешнего поведения ленточных автоматов и его разработка в свете решения проблем с несогласованной системой понятий. // Известия РАН. Теория и системы управления. 1996. №5.

6. Абрамова H.A. Развитие нового математического аппарата для анализа и верификации программ. // Труды Института, том XI. -М.: ИЛУ РАН, 2000. с. 39-61.

7. Абрамова H.A. Технологии проектирования вычислительных средств с использованием методов, основанных на формализации знаний. //Вычислительная техника. Системы. Управление. Междунар. сб. М.: МЦНТИ, 1991, вып.6, стр.52-67.

8. Abramova N.A., A Diagnostic Program Model. // Proc. of the 3rd Symp. on Technical Diagnostics. Budapest, 1983.

9. Abramova N.A. On Proving Testing Strategies // Technical Diagnostics 89. The House of Technology. Prague, 1989, Part 1,p.232-236.

10. Abramova N.A, Improving the Computing Facilities Diagnostics Quality by Logical Reasoning Formalization. // Technical Diagnostics 90, Helsinki, 1990. p.411-418.

11. Абрамова H.A., Коврига C.B., Измайлов О.А. Модельный подход к построению формализованных спецификаций. // Технологические средства создания систем управления. Доклады международной конференции. Кэярику, 04-07.05. 1992. Т.1, с. 131-149

12. Абрамова Н.А., Рубцова Э.Е., Соколов В.А. Модели внешнего поведения ациклических программ для машин потоков данных. // Моделирование и анализ информационных систем. Ярославль: ЯрГУ. 1994, с.3-12.

13. Абрамова H.А, Клочков А.И., Коврига C.B. Некоторые критерии адекватности решения научно-прикладных задач // Труды межд. конф. «Параллельные вычисления и задачи управления». РАСО 2001. -М.: ИПУ РАН, 2001, с. 3-19.

14. П.Абрамова H.A., Баталина Т.С., Гегамов H.A., Коврига C.B. Новый математический аппарат для анализа внешнего поведения и верификации программ. // Препринт. М.: ИПУ, 1998, 109 с.

15. Абрамова H.A., Коврига C.B., Сперанская И.В. Формализованные модели архитектуры процессоров и методика их построения. // Препринт, М.: ИПУ. 1989, 52 с.

16. Абрамова H.A., Амбарцумян A.A., Коврига C.B., Рубцова Э.Е. Методика верификационной отладки функциональных схем алгоритмов. // Препринт. М.: ИПУ. 1990, 52 с.

17. Абрамова H.A., Сперанская И.В. Развиваемая семантическая модель как механизм формализации знаний / / Тез. докл. Всес. конф. по искусственному интеллекту, Переславль-Залесский, 1988, т.1, с.44-48.

18. Абрамова H.A. Экспертно-логический подход к повышению достоверности обоснования // Тез. докл. 2-ой Всес. конф. по искусственному интеллекту. Минск, 1990, с. 12-13.

19. Абрамова H.A.,Коврига C.B., Разбегин В.П. Об одном подходе к порождению формализованных знаний и его возможностях. Труды Конф. КИИ'98, том 1, 192-196, Пущино, 1998.

20. Н.А.Абрамова. Об одном подходе к анализу разнородных методов повышения надежности ПТС и их совместимости. //Надежность, №1,2001, с. 24-37.

21. С.М.Абрамов. Тестирование программ с использованием окрестного анализа. Вопросы кибернетики. Проблемно-ориентированные вычислительные системы: М., 1987

22. Агафонов В.Н. Спецификация программ: понятийные средства и их организация.- Новосибирск: Наука, 1987.

23. В.Н.Агафонов. Система ПТО и технология спецификации программ. УСиМ,1988,№ 4,стр.54-58.

24. В.Н.Агафонов. Надъязыковая методология спецификации программ .- Программирование, № 5,1993

25. Г.С.Альтшуллер, Б.Л.Злотин, А.В.Зусман, В.И.Филатов. Поиск новых идей: от озарения к технологии (Теория и практика решения изобретательских задач). Кишинев. Картя молдовеняскэ. 1989.

26. Амбарцумян A.A., Искра С.А. Структурированные модели систем логического управления. Тезисы докладов, IX Всесоюзное совещание по проблемам управления, Ереван, 1983, М.: ИАТ-1983, с.294-295.

27. Амбарцумян A.A. Методология разработки распределенных систем управления технологическими процессами с повышенным экологическим риском. П и СУ, -1994, №11, с.28-31.

28. Ю.В.Бакалов, Р.Л.Смелянский. Язык спецификации поведения распределенных программ. Программирование, 1996, №5, стр.4152.

29. Барздинь Я.М., Заринып А.К., Калниньш A.A. Об одном языке спецификации. //Кибернетика, 1982, №6, стр.30-39

30. Безбородов Ю.М. Индивидуальная отладка программ. //М.: «Наука», 1982г.

31. А.И.Берг, Б.В.Бирюков, А.А.Столяр. Операторно-логическая "модель" мышления и обучения и кибернетическая педагогика. -Вступительная статья к книге 42., стр.9-21

32. Вейль Г. Математическое мышление: Пер. с англ. и нем./ М.: Наука. Гл. ред. физ.-мат. лит., 1989. - 400 с.

33. Дж.П. Боуэн, М.Дж. Хинчи. Десять заповедей формальных методов. PC World, 1997, №9

34. Величковский Б.М., Зинченко В.П., Лурия А.Р. Психология восприятия. М., 1976.

35. Вендров A.M. CASE-технологии. 7/М.: Финансы и статистика, 1998. 176 стр.

36. Ж. Верньо. К интегративной теории представления.// Иностранная психология, т.3,1995, №5

37. Воинов А., Гаврилова Т. Инженерия знаний и психосемантика: об одном подходе к выявлению глубинных знаний. // Изв.РАН Техническая кибернетика, 1994, N5.

38. В.А.Галатенко, П.В.Христов. Инкрементальные методы анализа программ. Программирование, 1991, No4, стр. 3-11.

39. Гаврилова Т.А., Червинская K.P. Извлечение и структурирование знаний для экспертных систем. М.: "Радио и связь", 1992

40. В.М.Глушков, Ю.В.Капитонова, А.А.Летичевский, О применении метода формализованных технических заданий к проектированию программ обработки данных. Программирование. 1999. С.27-37 (перепечатка статьи 1979 г.)

41. К.К.Гомоюнов. Лингвистическая терапия естественно-научных и технических знаний. Новости искусственного интеллекта. 1. 94

42. ГОСТ 28195-89. Оценка качества программных средств. Общие положения.53. ГОСТ Р ИСО/МЭК 9126-93.

43. Дружинин В. В., Конторов Д. С. Проблемы системологии. М.: Сов. радио, 1976.

44. Дейкстра Э.Дисциплина программирования. /Пер. С англ. -М.:Мир, 1985, 336 стр.

45. А.П. Ершов. Некоторые субъективные замечания к актуальным проблемам программирования. Перспективы системного итеоретического программирования. Труды Всес. симп. АН СССР, Сибирское отделение, Вычислительный центр, Новосибирск, 1979.

46. А.П.Ершов. Введение в теоретическое программирование (беседы о методе). М.: Наука. Гл. ред. физ.-мат. лит., 1977. - 288 с

47. Кузенко В.Ф. Отношения именования и программные алгебры языков высокого уровня. Программирование, 1994, 2, 79-85.

48. Кузнецов О.П. Теория алгоритмических конечноавтоматных языков. 11. Сравнение языков по эффективности. Автоматика и телемеханика. 1981, №4, с. 156-164.

49. Кузнецов О.П. О программной реализации логических функций и автоматов. 1. Анализ и синтез бинарных программ. // А и Т. 1977.Ж7. С.25-39

50. Кузьмин А.К. Формальная верификация схемных и архитектурных решений. УСиМ, 1988, май-июнь, стр.7-11.

51. Лингер Р., Милз X., Уитс Б. Теория и практика структурного программирования. М.: Мир, 1982.

52. В.В.Липаев. Качество программного обеспечения. М.: Финансы и статистика, 1983.- 92 стр.

53. В.В.Липаев. Тестирование программ. //М. Радио и связь. 1986

54. Липаев В.В. Надежность программных средств. «Синтег», М., 1998.

55. Лисков Б., Гатэг Дж. Использование абстракций и спецификаций при разработке программ. М.: Мир, 1989.

56. Литвинцева Л.В. // Тез.докл. Всесоюзн. конф. по искусственному интеллекту, Переславль-Залесский, 1988. Т.1,С.569-572

57. Майерс Г. Надежность программного обеспечения. Пер. с англ. / Под.ред. В.Ш.Кауфмана. М.: Мир, 1980г., - 360 стр.

58. Найссер У. Познание и реальность. М.,1981.

59. Непейвода H.H., Логические и алгоритмические формализмы для задачи построения правильных программ. //Программирование, 1999, №3, с. 57-66 (перепечатка статьи 1979г.)

60. Непейвода H.H. О формализации неформализуемых понятий: автопродуктивные системы теорий // Семиотика и информатика. -М., 1985.Вып.25,стр.46-93

61. Непомнящий В.А., Сулимов A.A. Об одном подходе к спецификации и верификации транслятора. // Программирование, 1983, №4, 51-58.

62. Непомнящий В.А. Практические методы верификации программ. //Кибернетика, 1984, №2,21-28,43.

63. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М: Радио и связь, 1988.

64. Непомнящий В.Д. и др. Real 92: Комбинированный язык спецификаций для систем и свойств взаимодействующих процессов реального времени. Программирование, 1993, 6, 6481.

65. Осипов Г.С. Приобретение знаний интеллектуальными системами. Основы теории и технологии. М.: Наука. Физмат., 1997. - 110 с.

66. Петренко А.К. Спецификация тестов на основе описания трасс. -Программирование, 1993, 1, 66-74.78. 23. Подловченко Р.И. О проблеме эквивалентных преобразований программ. Программирование, изд."Наука", 1986, N6, стр.3-14.

67. Поспелов Д.А. Логико-лингвистические модели в системах управления. — М.: Энергия, 1981

68. Поспелов Д.А. Прикладная семиотика и искусственный интеллект // Программные продукты и системы. 1996, №3. - с. 10-13.

69. Поспелов Д.А. Десять «горячих точек» в исследования по искусственному интеллекту// Интеллектуальные системы (МГУ). -1996,Т.1, вып. 1-4. с.47-56.

70. Поспелов Д.А., Осипов Г.С. Прикладная семиотика //Новости искусственного интеллекта. Журнал Российской Ассоциации искусственного интеллекта. М.: 1999, №1, с. 9-35.

71. Прангишвили И.В., Абрамова Н.А., Спиридонов В.Ф., Коврига C.B., Разбегин В.П. Поиск подходов к решению проблем. М.: Синтег, 1999. 284 с.

72. Проектирование 32-разрядного процессора повышенной надежности. Электроника, N2, 1986, стр.30-35.

73. Редько В.Н. Основания композиционного программирования. Программирование. 1979, N3, стр.3-13.

74. Х.Роджерс. Теория рекурсивных функций и эффективная вычислимость. Мир, Москва, 1972.

75. Смелянский Р.Л. Применение темпоральной логики для спецификации программных систем. Программирование, 1993, 1, 3-29.

76. Сприридонов В.Ф. Закономерности онтогенетического развития продуктивного мышления. Вестник МГУ, сер. 14, Психология, 1994, N2, с. 13-24.

77. Тузов В.А. Об одном способе описания языков программирования. Программирование. №3, 1979

78. Трахтенброт Б.А., Барздинь Я.М. Конечные автоматы. Поведение и синтез. М.: Наука, 1970.

79. Успенский В.А., Семенов А.Л. Теория алгоритмов: основные открытия и приложения. М.: "Наука", 1987. - 288 с.

80. Фридерике Никль и др. Формальный подход к инженерии требований. Программирование, 1993, 6, 39-64

81. Цейтлин Г.Е., Ющенко Е.Л. Алгебра алгоритмов и граф-схемы Калужнина. Кибернетика и системный анализ, 1994, №2, стр.3-17. (Графовые и аналитические спецификации алгоритмов)

82. Чеботарев А.Н. Проверка непротиворечивости простых спецификаций автоматных систем. //Кибернетика и системныйанализ, 1994, № 3, стр.3-11. (Институт кибернетики им. В.М.Глушкова АН Украины)

83. Чень, Ли Р. Математическая логика и доказательство теорем./Перевод с англ. М.:Наука, 1983,- 358 стр.

84. Шапиро С.И. Мышление человека и переработка информации ЭВМ. М.: Сов. радио, 1980. - 288 с.

85. Юдицкий С.А., Маргегут В.З. Логическое управление дискретными процессами. М.: Машиностроение, 1987.

86. Ackerman, A.F., Ackerman, A.S., Ebenau, R.G., "A software inspections training program", Computer Software and Applications (COMPSAC-82). Proc. Conf. New York (Nov. 1982).

87. Adrion, W.R., Branstad, M.A., Cherniavsky, J.S., Validation, Verification and Testing of Computer Software, National Bureau of Standards Special Publication NBS-SP-500-75, NBS, Washington, DC (Feb. 1981).

88. American Nuclear Society, Guidelines for Verification and Validation of Scientific and Engineering Computer Programs, Draft Standard, Rep. ANSI/ANS-10.4, ANS, La Grande Park, IL (1987).

89. Andrewartha, N., "Project Management of Computer Based Safety Critical Systems", Software Engineering inNPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

90. ANSI/IEEE, Standard for Software Quality Assurance Plans, Standard 730, Institute of Electrical and Electronics Engineers, Inc., New York (1984).

91. ANSI/IEEE, Standard for Software Unit Testing, Standard PI 0081987, Institute of Electrical and Electronics Engineers, Inc., New York (1987).

92. J.Backus, "Can programminq be liberated from the von Neuman style? A functional style and its algebra of programs," Comm. ACM, Vol.21, No. 4,(1978)

93. G. Barren, Model Checking in Practice: The T9000 Virtual Channel Processor IEEE TRANSACTIONS ON Software Engineering, Vol. 21, No. 2., February 1995, pp.69-78

94. H.Barringer, J.H.Cheng, and C.B.Jones, A Logic Covering Undefinedness in Program Proofs Acta Informática, 1984,v.21, 25129.

95. Baldwin, J. A., Wall, D.N., "A Brief Examination of the Difficulties of Using Software for Nuclear Safety Applications", Software Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

96. Barnes, M., Bradley, P.A., "Software Licensing & Assesment-Problems and Solutions", Software Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

97. Basili, V.R., Perricone, B.T., Software errors and complexity: An empirical investigation, Commun. ACM 27 1 (Jan. 1984).

98. V.R.Basili, R.E.Noonan. A Comparison of the Axiomatic and Functional Models of Structuered Programming. IEEE Transactions on Software Engineering, 1980, September, v.SE-6, N5, pp.454-464.

99. D.M.Berry. Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language. "IEEE Trans. Software Eng"., vol. SE-13, No. 2, February, 1987

100. P.R.Bhattacharjee and others. Translation of the problem of complete test set generation of complete test set generation of pseudo-booling programming. Computers, 1991, v.40,n.7,864-867.

101. Bhatt, S.C. Chanel,1., "Comparison of International Standards for Digital Safety System Verification & Validation", Software

102. Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

103. Bologna.S., Rao, D.M., "Application of Independent Software Verification to Microprocessor based Nuclear Power Plant Protection Systems", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

104. J.P.Bowen. Formal Specification and Documentation of Microprocessor Instruction Sets. "Microprocessing and Microprogramming", vol.2 , 1987, pp. 223-230

105. Branstad, M.A., (NBS), Cherniavsky,J.C., (NBS), Adrion,W.R., (NSF), Validation, Verification and Testing for individual programmer, Computer, v. 13, № 12 (Dec. 1980) 24.

106. Brown,J.R., "Programming practices for increased software quality" Software Quality Management, Petrocelli Books, New York and Princeton (1979), pp. 197.

107. Bruce P., Pederson S.M., The Software Development Project -Planning and Management, Wiley, New York (1982).

108. F.Buckley, A standard for software quality assurance plans. Computer 12, 8, (Aug. 1979), 43-50

109. B.Cohen. Justification of Formal Methods for System specification. S8oftware & Microsystems, Vol.1, No.5, August 1982 p. 119-124.

110. Cain, J.T., Langdon,G.G., Varanasi,M.R., "The IEEE computer society model program", Computer Science and Engineering, Computer 17 4 (Apr. 1984), 8.

111. L.C. Carpenter and L.L.Tripp."Software design validation tool", in Proc. 1975 Int. Conf. Reliable Software (Apr. 1975)

112. P. Camurati, P. Prinetto. Formal Verification of Hardware Correctness: Introduction and Survey of Current Research. -Computer, 1988, July, pp.8-19.

113. Chusho T .Test Data Selection and Quality Estimation Based on the Concept of Essential Branches for Path Testing, TSE, vol. se-13, No.5 May 1987, pp.509-517

114. Condor, A.E., Hinton, G.J., "Fault Tolerant and Failsafe Design of CANDU Computerized Shutdown Systems", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

115. Courtois, P.-J., Parnas, D.L., "Documentation for Safety Critical Software", Software Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

116. S.Dasgupta. On the verification of computer architectures using an architecture description language.- Proceedings of the 10th Annual International Symposium on Computer Architecture (Stockholm). IEEE Press, New York, 1983, 32-38.

117. Dasgupta S.The Design and Description of Computer Architectures. New York: Willy, 1984.

118. Daughtrey, T., Levinson S., "V&V of and by Expert Systems", Methodologies, Tools, and Standards for Cost Effective, Reliable Software V&V, Proc EPRI Conf., EPRI TR-100294, Palo Alto, CA, (Jan, 1992).

119. Dyer M. A Formal Approach to Software Error Removal // The Journal of Systems and Software, 1987, v.7, N 2, p.p.100-114.

120. DeMillo R.A., Lipton R.J., and Sayward F.G., Hints on

121. Test Data Selection: Help for the Practicing Programmer, Computer 34-37 (April 1978)

122. DeMillo R.A.DeMillo R.A., Lipton R.J., and Perlis A.J., Social Processes and Proofs of Theorems and Programs, Comm.ACM, ,V.22, No.5, May 1979, p.271-280

123. DeMarco,T., Controlling Software Projects Management Measurement and Estimation, Yourdon Press, New York (1982).

124. Deutcsch, M.S., Software Verification and Validation Realistic Approaches, Prentice Hall, Englewood Cliffs, NJ (1982).

125. Dijkstra E. W., "The Goto Statement Considered Harmful," Comm. ACM, Vol.11, No.3, pp.73-74 (1968).

126. B.Elspas, K.N.Lewitt, R.J.Waldinger, A.Waksman. An assessment of techniques for proving program correctness. ACM Computing Surveys, 1972, v.4, n.2, 97-147

127. Endres,A., An analysis of errors and their causes in system programs, IEEE Trans. Software Eng. SE-1 2 (Jun. 1975).

128. Fagan M.E., Advances in Software Inspections, IEEE Trans, on Software Engineering, v.SE-12, N 7, (1986).

129. R.Floyd. Assigning meaning to programs. Mathematical Aspects of Computer Science, XIX, Amer. Math. Soc., 1967, p.p. 19-32.

130. Foster, K.S., Error sensitive test case analysis (ESECA), IEEE Trans. Software Eng. SE-6 3 (May 1980) 258.

131. A.Gabrielian and M.K.Franclin. Multilevel specification of real-time systems. Communications of the ACM, 1991, v.34, n.5, p.p.50-61

132. Gannon, C., Error detection using path testing and static analysis, Computer 12 8 (Aug. 1979) 26

133. Gannon,C., "Software error studies", Proc. Nat. Conf. on Software Test and Evaluation, National Security Industrial Assotiation (Feb. 1983)1-1

134. Glass, R.L., Software Reliability Guide Book, Prentice Hall, Englewood Cliffs, NJ (1979).

135. Glass,R.L., Persistent software errors, IEEE Trans. Software Eng. SE-7 2 (Mar. 1981) 162-168.

136. C.P.Gerrard, D.Colleman, and R.M. Gallimore, Formal Specification and Design Time Testing.- IEEE Transactions on Software Engng V.SE-16, No 1, Jan. 1990, pp.1-11.

137. V.D.Gligor, C.S.Chandersekaran, W.D.Jiang, Johri, G.L.Luckenbaugh, L.E.Reich. A New Security Testing Method and Its Application to the Secure Xenix Kernel. IEEE Transactions on Software Engineering, 1987, v.SE-13, n.2, 169-183.

138. J.D.Gannon, R.G.Hamlet, and H.D.Mills, "Theory of Modules", IEEE Trans. Software Eng., Vol.13, No.7, July 1987, pp.820-829

139. Gregory, R.A., "Programmable Logic Controllers in Safety Related Applications", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

140. J.Guttag. "Notes on Type Abstraction (Version 2)", IEEE Trans. Software Eng., Vol.6, No.l, Jan. 1980, pp. 13-23

141. Guttag J.V., Horning J.J. Larch: Languages and tools for formal specification. Berlin a.o.: Springer, 1993

142. J. B. Goodenough and Susan L. Gerhart. Theory of Testdata selection, IEEE Trans, on Software Engineering, Vol. SE-1, No2, June 1975, pp.156-173.

143. F.K.Hanna and others. Specification and verification using dependent types. IEEE Transactions on software engineering, 1990, v. 16, n.9, 949-964.

144. Hamilton, V., "Formal and Conventional Development Methods -Complementary Techniques for Error Elimination", Software engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

145. C.Heitmeyer, J.Kirby, Jr., B.Labaw, M.Archer, R.Bharadway/ Using abstractions and model checking to detect safety violations in requirements specifications. IEEE, Trans. Softw. Eng. Vol.24, No. 11 (Nov. 1998), pp.927-947.

146. C.A.R.Hoare. An axiomatic basis for computer programming. -Communications of the ACM, 1969, v. 12, n.10, 576-583

147. W.E. Howden, "Reliability of the path analysis testing strategy", IEEE, Trans. Softw. Eng. SE-2,3 (1976).

148. Howden,W.E., "Errors, design properties and functional program tests", Computer Program Testing, North-Holland, Amsterdam and New York (1981) 115.

149. W. E. Howden, Theoretical and Empirical Studies of Program Testing,- IEEE Trans.on SE, vol. SE-4, No.4 July 1978, pp.293-298

150. W. E. Howden, A Functional Approach to Program Testing and Analysis, TSE, vol. SE-12, No. 10, October 1986, pp.997-1005

151. Huang, J.C., "Error detection through program testing", Current Trends in Programming Methodology, Vol.2, Program Validation, Prentice Hall, Englewood Cliffs, NJ (1977) 16

152. Institute of Electrical and Electronics Engineers, Inc., Tutorial: Software Testing and Validation Techniques, IEEE Computer Society Catalog No. EH0138-8, IEEE, New York (1978).

153. International Electrotechnical Commission, Software for Computers in the Safety Systems of Nuclear Power Stations, IEC Standard 880, Geneva (1986).

154. ISO 9126: 1991. ИТ. Оценка программного продукта. Характеристики качества и руководство по их применению.

155. An invitation to formal methods. H.Saiedian, J.P.Bowen, R.Butler, D.Dili, R.Glass, D.Gries, A.Hall, M.Hinchey, C.Holloway, DJackson, C.Jones, M.Lutz, D.Parnas, J.Rushby, J.Wing, P.Zave. Computer, 1996, v.29,April,|4, p.p.16-33

156. P.Jain, S.S.Lam. Specification of real-time broad-cast networks. Computers, 1991, v.40,n4, 404-423.D.

157. Y.Kakuda, H.Satio. An integrated approach to design of protocol specifications using protocol validation and synthesis. Computers, 1991, v.40, n4, 459-468.

158. K.Katsuyama and others, Strategic testing environment with formal description techniques. Computers, 1991, v.40,n4,514-526.

159. Kendrick, S.H., Keates, A.A.G., Russomanno, S.A., Sutherland, J.G., "Verification & Validation of the CANDU Safety System Computer Software", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

160. Kerola,P.,Freedman,P., "A comparison of life-cycle models", Proc. 5th Int. Conf. on Software Engineering, IEEE computer Society Catalog No 81 CHI 627-9, Institute of Electrical and Electronics Engineers, Inc., New York (1981) 90.

161. Laski J.W., A Hierarhical Approach to Program Testing. IEEE Transactions on Software Engineering, 1979, 66.77-85

162. Laski J.W.,Korel B. A Data Flow Oriented Program Testing Strategy.-IEEE Transactions on Software Engineering, 1982, May, v. SE-9,N3,,pp 347-354.

163. N.Levenson, "Software Safety: Why, What and How," Computng Surveys, vol. 182,No.2,1986, pp. 125-163.

164. Y.Lee, J.Y.Lee. A well-defined estelle spesification for the atomatic test generation. Computers, 199l,v.40,n4,526-543.

165. L.S.Levy and R.Melville. The algebraic anatomy of programs. The Computer Journal, V.20, No.4,1977, p.340-345.

166. L.S.Levy. A Metaprogramming Method and Its Economic Justification. IEEE Transactions on Software Eng., vol.SE 12, No.2, february, 1986

167. R.L.London. A view of program verification. Proc. of Int. Conf. on Reliable Software. Los Angeles, 1975, p.p.534-545

168. T.P.Luchido, R.Chattergy, U.W.Pooch. A survey of microprogram verification and validation methods. The Computer Journal, 1981, v.24, n.2, 139-142

169. M.J.Mahon. Hewlett-Packard Precision Architecture: The Processor.- "Hewlet-Packard Journal", August 1986

170. Matras, J.R., "Planning is not Sufficient Reliable Computers Need Good Requrements Specifications", Methodologies, Tools, and Standards for Cost - Effective, Reliable Software V&V, Proc EPRI Conf., EPRI TR-100294, Palo Alto, CA, (Jan, 1992).

171. Z.Manna. The correctness of programm. Journal of Comp. and Sy. Sci., 1969, n.3, 119-127.

172. Manna Z., "Properties of Programs and First-Order Predicate Calculus", JACM, April 1969.

173. Manna, Z., Mathematical Theory of Computation, McGraw-Hill, New York, 1974

174. Manna Z., Waldinger R., The Logic of the Computing Programming, IEEE Transactions on Software Engineering, Vol. SE-4, No. 4., May 1978, pp.199-229.

175. E.F. Miller. Program Testing: Art Meets Theory.Computer, July 1977, pp.42-51

176. H.D.Mills, "Top Down programming in large systems,"in Debugging techniques in large systems, R.Rustin (Ed.), Prentice-Hall, Englewood Cliffs, N.J., 1970, pp.41-55

177. H.D.Mills, "The New Math of Computer Programming", Comm. ACM, Jan. 1975, v. 18, No.l, pp.43-48

178. Mills H.D. Structured programming: retrospect and prospect // IEEE Software. 1986. v.3. №6. p.58-66

179. H.Mills, R.C.Linger. "Data Structured Programming: Program Design without Arrays and Pointers".- IEEE Trans, on Software Eng., vol.SE-12,No. 2, February 1986.

180. Mills, H.D. Functional Semantics for Sequental Programs.- Proc. of the IFIP Congress '80, pp.241-250, North Holland Publishing Co., Amsterdam, 1980.

181. Mills, H. D., Basili, V.R, Gannon, J. D., and Hamlet, R. G., Principles of Computer Programming: A Mathematial Approach, Allin and Bacon, 1987

182. Mizumoto, T., et al., "Microprocessor based Reactor Protection System for PWR Plants in Japan", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

183. Naser, A., Bhatt, C., "In Search of Cost-Effective, Reliable Software", Methodologies, Tools, and Standards for Cost-Effective, Reliable Software V&V, Proc EPRI Conf., EPRI TR-100294, Palo Alto, CA, (Jan, 1992)

184. Paidge M.M., Balkovich E.E. On Testing Programs. "IEEE Symp.Comput. Software Reliability, New York City, 1973", Proc., New York, N.Y. 1973

185. D.L. Parnas, "Mathematical Descriptions and Specification of Software," Proc.IFIP World Congress 1994, Vol. I, Aug. 1994, pp. 354-359.

186. D.L.Parnas et.al., "Evaluation of Safety-Critical Software", Comm.ACM, vol.33, No. 6, June 1990, pp.636-64.

187. Parnas, D.L., et al., "Evaluation Standards for Safety Critical Software", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

188. R.E. Prather, J. P. Myers. The Path Prefix Software Testing Strategy. -TSE, vol. se-13, No.7 July 1987, pp.761-765

189. D. J.Richardson & M. C.Tompson. An Analysis of Test Data Selection Crteria Using the RELAY Model of Fault Detection TSE vol.l9,No.6, June 1993, pp.533-553

190. R. P. Roe, J. H. Rowland. Some Theory Concerning Certification of Mathematical Subroutines by Black Box Testing TSE, vol. se-13, No.6 June 1987, pp.677-682

191. K.Ramamritham, R.M.Keller. Specification of synchronizing processes. IEEE Transactions on Software Engineering, 1983, v.SE-9, n.6, 723-733.

192. Rusinkiewicz M. and others. Specifying interdatabase dependencies in a multidatabase environment. Computer, 1991, v.24, n.12, 46-55.

193. H.Saiedian, J.P.Bowen, RButler, D.Dill, R.Glass, D.Gries, A.Hall, M.Hinchey, C.Holloway, D.Jackson, C.Jones, M.Lutz, D.Parnas, J.Rushby, J.Wing, P.Zave. An invitation to formal methods. -Computer, 1996, v.29,April,№4, p.p. 16-33.

194. Sadler, S.J., Robinson, P., "The Use of Formal Methods in the Development of Safety Critical Software", Microprocessors in Systems Important to the Safety of NPPs, Proc. IAEA Spec. Meeting, London (May 1988).

195. G.M.Silberman, I.Spillinger, RIDDLE: A foundation for test generation on high-level design description. Computers, 1991, v40, nl, 80-88.

196. G.M.Sieberman, I. Spillinger. Functional faultsimulation as a quide for beased-random test pattern generation. -Computers, 1991 ,v40,nl ,66-80.

197. Shankar,K.S., The total computer security problem: An overview, IEEE Computer 10 6 (Jun. 1977) .

198. Shen,V.Y., YU,T.J., Thebaut, S.M., Paulsen, L.R., Identifying error -prone software An empirical study, IEEE Trans. Software Eng. SE-11 3 (Mar. 1985)

199. Soubies, B., Le Meur, M., Henry, J.Y., Boulch J., "Safety Software Evaluation Methods in the I&C of Nuclear Power Plants", Software Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

200. Straker E. A., Thomas N. C . Verification and Validation as an Integral Part of the Development of Digital Systems for Nuclear Applications //Nuclear Safety, 1983, v.24, N 3, p.338-351

201. P.Tripathy, B.Sarikaya, Test generation from Lotos specifications.-Computers, 1991,v40,n4,543-553.

202. Vankay, J., "The Integrated Approach System Design Methodology", Software Engineering in NPPs, Proc. IAEA Spec. Meeting, Chalk River, (Sept. 1992).

203. F.R.D. Velasco. A method for test data selection.- The Journal of Systems of Software, 7, 89-97 (1987)

204. Wirth N., Program Development by Stepwise Refinement // Comm/ ACM. 1971. V. 14. n.4.

205. L.Yang . Constructing optimal procedures for testing series systems. Computers, 1990, v.39,n7,943-945.

206. P. Zave and M.Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Trans, on SE, vol.22, No.7, July 1996, p.508-527.

207. P.Zave. An insider's evaluation of PAISLey. IEEE Transactions on Software Engineering, 1991,v.17, n.3, p.p.212-225.252

208. M.V.Zelkovitz, A Functional Correctness Model Of

209. Program Verification.- Computer, Vol.23, No.l 1, Nov. 1990, pp.3040.

210. Ионин JI.Г. Понимание и экспертиза // Вопросы философии, №10, 1991.

211. Кубрякова Е.С. Словарь когнитивных терминов. М.: МГУ, 1996

212. Д. Пойа. Математика и правдоподобные рассуждения. М.: Наука, 1975. - 463 с

213. Пойа Д. Математическое открытие. Решение задач: основные понятия, изучение и преподавание. М.: 2-е издание, 1976. 448 с.

214. К. Поппер. Логика и рост научного знания. М.: Прогресс, 1983. - 605 с.

215. Спиридонов В.Ф. Роль эвристических средств в развитии процессов решения творческой задачи. // Вестник Московского Университета, сер. 14 "Психология" N 2, 1993, с. 13-21.

216. Шапиро С.И. От алгоритмов к суждениям (Эксперименты по обучению элементам математического мышления.) - М.: Сов. радио, 1973. - 288 с.

217. Norman D.A. The role of active memory processes in perception and cognition. Proceedings of the 21 Internal Congr. of Psychol. Paris, 1978.

218. КРАТКОЕ ОПИСАНИЕ МЕТОДИК ВЕРИФИКАЦИИразработанных при выполнении комплекса работ по верификации проекта «Рабочее программное обеспечение и конфигуратор для АЭС «Бушер» (заказчик ФГУП «Атомэнергопроект», г. Москва) 2001 г.

219. Методики разработаны в соответствии методологией повышения надежности проектирования ПТС, представленной в диссертации.

220. Методика экспертного анализа качества ПД1

221. Методика проверки качества описания семантики языка посредством построения модели вычислений

222. Цель методики проверка качества описания семантики языка на понятность, полноту, однозначность и непротиворечивость.

223. Методика накладывает ряд частных критериев на качество определения ключевых нетерминальных понятий языка и их взаимосвязи.

224. Методика оценки тестируемости ПД посредством модели функциональности

225. Под тестируемостью ПД понимается возможность определения поведения документируемого объекта во всех вариантах поведения на основе описания в ПД.

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

227. Результат экспертная оценка тестируемости ПД

228. Процесс применения методики:1. Этап 1.

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

230. На основании сформулированного критерия в анализируемом ПД выявляются непонятность, неполнота, неоднозначность, нечеткость, противоречивость ПД (относительно модели).

231. Уровень тестируемости при наличии общей модели оценивается, в основном, в зависимости от:1. понятности и четкости исходного описания,2. полноты и непротиворечивости.

232. Методика оценки верифицируемое™ программы на основе ПД посредством модели функциональности

233. Методика проверки качества семантики интерфейса

234. Описываемая методика накладывает ряд частных критериев на качество описания семантики интерфейса.

235. Методика оценки тестируемости ПД посредством модели функциональности

236. Под тестируемостью ПД понимается возможность определения поведения документируемого объекта во всех вариантах поведения на основе описания в ПД.

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

238. Результат экспертная оценка тестируемости ПД.

239. Процесс применения методики:1. Этап 1.

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

241. На основании сформулированного критерия в анализируемом ПД выявляются непонятность, неполнота, неоднозначность, нечеткость, противоречивость ПД (относительно модели).

242. Уровень тестируемости при наличии обшей модели оценивается, в основном, в зависимости от:1. понятности и четкости исходного описания,2. полноты и непротиворечивости.

243. При этом требования (1) имеют более высокую значимость, чем (2): если понятность и четкость исходного описания недостаточны, неполнота и противоречивость не обнаруживаются.

244. Оценки должны определяться с учетом назначения ПД и категорий пользователей.

245. Методика экспертного анализа влияния инструментального комплекса ИПО РПО на критические показатели качества ИПО СВБУ

246. Условия применения методики

247. Правила обработки исходных требований (после идентификации типа требования)

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

249. Двусмысленные требования рассматриваются, в первую очередь, как косвенные для ИПО РПО (например, правильность в первую очередь рассматривается как правильность ИПО СВБУ) и, по возможности, как прямые к ИПО РПО.

250. Далее по тексту отчета введено обозначение сетевой библиотеки СБдвусмысленных требований. (Например, не устанавливалось требование правильности к инструментарию комплекса ИПО РПО.)

251. Методика экспертного анализа функциональности ИПО СВБУ

252. Методика предназначена как вспомогательная для оценки влияния программных средств и технических решений, представленных в комплексе ИПО РПО, на критические показатели ИПО СВБУ, такие как правильность, устойчивость, настраиваемость на специфику АСУ ТП.

253. Для целей оценки проводится экспертный анализ функциональности систем ИПО СВБУ, создаваемых на основе ИПО РПО.

254. Модель должна разделять уровни иерархии в ИПО СВБУ и связанные с ними критерии правильности, с учетом большей значимости критериев верхних уровней.

255. Исходные данные для применения методики первичное описание функциональности ИПО СВБУ, создаваемой на основе ИПО1. П- 11

256. РПО, которое представлено в верифицируемых документах ПД1, ПД2 и привлеченных документах проекта: ЧТЗ 1., Пояснительная записка 2.

257. Согласно методике, с применением авторских методов разработки моделей функциональности, построена модель функциональности ИПО СВБУ.

258. Модель прошла отладку в ходе верификации ПД1, ПД2, в том числе, в рамках применения методик оценки поддержки правильности и устойчивости ИПО СВБУ средствами ИПО РПО, настраиваемо-сти на специфику АСУ ТП.

259. Элементы тракта GATE-CGP в целом, которые рассматриваются на следующем уровне, это целостные программы GATE, CGP и их интерфейсы: GATE-смежные ПТК, GATE-CGP, CGP-DB.

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

261. На уровне отдельных крупных функций программ (как видно по результатам анализа в табл.7.5.2) выделяются функции «от входа довыхода» программ GATE и CGP3 и поддерживающие их функции инициализации.

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

263. Частные применения общей методики

264. Оценка по оценочному фактору третьего уровня (субфактору) «наличие и качество сведений для поддержки правильности реализации функций тракта вАТЕ-ССР в ИПО СВБУ » проводится в полном соответствии с общей методикой.

265. Оценка по оценочному фактору второго уровня «охват функций ИПО СВБУ библиотеками» в рамках фактора первого уровня «соответствие требованиям универсальности ИПО РПО» проводится в полном соответствии с общей методикой.

266. Методики экспертного анализа и оценки по фактору «Наличие и качество сведений по процессу создания ИПО СВБУ на основе ИПО РПО»

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

268. При этом поддержка тем глубже, чем более технический характер приобретает процесс создания ИПО СВБУ на основе ИПО РПО (в области охвата этого процесса).