Cтраница 3
Часто кластерные методы используются в сочетании с языками спецификации, инвариантными относительно технической реализации функций архитектуры. Так, в [73] в качестве языка спецификации используется UNITY, который изначально разрабатывался как средство и метод спецификации параллельных вычислений. Этот язык сочетает в себе возможности нотации и формальной верификации программ. Язык позволяет описать синхронное и асинхронное взаимодействие процессов без их предварительного планирования и назначения на ресурсы. Таким образом поддерживается функциональный стиль спецификации и возможность анализа конкретных реализаций компонентов архитектуры в широком диапазоне - от программ до заказной аппаратуры. Близким к рассмотренному в [73] является метод объектно-ориентированных функциональных спецификаций [159], в котором используются теоретике-множественные нотации архитектуры. Состояние системы представляется объектами, которые реализуются как функции языка СП-К Намеренный уход от операционной семантики в спецификациях обеспечивает гибкость в реализации архитектурных решений. [31]
Описано ядро защиты операционной системы, разработанной фирмой UCLA. Сначала рассмотрены общие принципы построения ядра защиты и введено понятие виртуальных машин, на которых основана методика разработки ядра системы UCLA. Затем рассмотрена система UCLA-VM и обсуждены успехи, достигнутые при разработке процедур верификации программ. Проанализирована зависимость стоимости такого ядра защиты от его структуры, предоставляемых пользователю гарантий защиты информации и быстродействия. Авторы приходят к заключению о том, что в вычислительных системах коллективного пользования проверенная программно-реализуемая защита может быть использована на практике. [32]
Заметим, что если этот интервал пуст, то в соответствии со спецификацией S целевое утверждение G не должно иметь решений. В общем случае решения, разумеется, существуют; чтобы подчеркнуть соответствие решений спецификации S, каждое такое решение tS назовем специфицируемым решением G. Является ли оно также решением, вычисляемым программой, - совсем другой вопрос, и именно на этот вопрос должна дать ответ верификация программы. [33]
Это и есть реализация второго метода конкретизации - метода последовательных приближений. Идея его состоит в том, что если есть какой-то способ за один шаг немного приблизиться к решению и его можно повторять много раз, то рано или поздно мы несомненно получим полное решение. Точное определение метода последовательных приближений очень важно, и мы еще вернемся к нему позднее в том месте этой главы, где будет обсуждаться верификация программ. Для приведенного выше примера предположим, что элементы данных могут быть пронумерованы от 1 до N н что оператор ввести часть данных вводит по крайней мере один элемент данных. Можно заключить отсюда, что для получения полного решения понадобится не более N шагов. [34]
Подробное изложение теории доказательства правильности программ или их верификации, как обычно называют этот процесс, не входит в задачу этой книги. В самом деле, концепции, используемые при верификации программ, представляют собой не более чем формализованные версии идей, возникающих в голове хорошего программиста, когда он пишет программу. [35]
Правильность программы определяется как соответствие между программой и ее заданной функцией. Для сведения задачи доказательства правильности определенной составной программы к задаче доказательства правильности определенных элементарных составляющих программ привлекают алгебраические понятия. Верификация правильности программ без циклов осуществляется с помощью анализа соответствующих Е - схем. Лемма о переходе от итеративных программ к рекурсивным позволяет свести задачу верификации циклических программ к задаче верификации эквивалентных программ без циклов. В теореме правильности обобщены требования к верификации, соответствующие ациклическим и циклическим элементарным программам. Для доказательства правильности программ используются трассировочные таблицы и разделяющиеся условные правила. Теоретико-функциональный подход к верификации иллюстрируется несколькими примерами. Еще один способ доказательства правильности циклических программ основан на использовании инвариантов цикла. Инварианты применяются также в качестве вспомогательного средства документирования программ. Для определения инвариантов дана общая процедура, основанная на теореме об инварианте. Наконец, с целью углубления в процесс проектирования программ приводится метод вывода правильных программ, использующий функциональные уравнения элементарных программ, для которых существуют формальные решения. [36]
Приведены некоторые частичные результаты научно-исследовательских разработок по созданию ядра защиты системы Multics. Описаны исследования, выполненные до начала этой работы, даны формулировки задач, объяснено, почему система Multics наиболее приспособлена для достижения поставленных целей. Основная часть доклада посвящена описанию трех принципов, положенных в основу этого проекта. Первый принцип заключается в удалении из состава ядра всех несущественных деталей, второй - в реконструировании оставшейся части ядра, третий - принцип модульности - позволяет упростить верификацию программ. [37]
Процесс чтения плоха документированной программы снизу вверх называется поэтапным абстрагированием. Последнее может потребоваться либо для верификации правильности, либо для определения программной функции программы. Если целевая функция программы задана, но промежуточные абстракции не известны, то программная функция должна быть определена и сравнена с целевой функцией. Если же промежуточные абстракции известны, то вначале они могут быть верифицированы путем их поэтапного абстрагирования с учетом деталей еще более низкого уровня, а затем использованы для верификации программы на более высоком уровне. [38]
Программа, записанная на любом из языков программирования, называется исходным модулем или исходной программой. Программы в объектном коде не являются еще машинными программами. Они не предназначаются для непосредственного выполнения, так как кроме текста программы содержат дополнительную информацию, позволяющую организовывать связи между отдельными частями программы. То, что здесь подразумевается под автоматическим программированием, можно описать как суперкомпилятор, или программу, способную воспринимать описание на понятном нам языке того, что требуется от искомой программы. Задача автоматического написания программы для достижения заданного результата тесно связана с задачей доказательства того, что программа достигает этого результата. Последняя задача называется задачей верификации программы. [39]
Статическое тестирование является наиболее формализованным и автоматизируемым методом проверки корректности программ. В качестве эталонов применяются правила структурного построения программных модулей и обработки данных, конкретизированные для проекта КП в целом. Кроме того, могут использоваться некоторые частные правила обработки данных, зафиксированные в спецификациях на отдельные компоненты. Проверка выполнения этих правил проводится без исполнения объектного кода программы путем формального анализа текста на языке программирования. Операторы и операнды текста программ анализируются в символьном виде, вследствие чего этот метод называют также символическим тестированием. Развитие и углубление символического тестирования может доводиться до уровня формальной верификации программ на соответствие ее текста детальной спецификации совокупности утверждений, полностью определяющей связи между входными и выходными данными этой программы. [40]