Верификация - программа
Cтраница 2
Приведенный выше пример отладочного приема показывает, что логические выражения, их упрощение, анализ и доказательство необходимы не только для верификации программ, но и для создания более упорядоченных методов программирования. [16]
Описаны результаты выполнения проекта большой операционной системы Multics, в которой применены технология ядра защиты, принципы управления информационным потоком и методы верификации программ. Поскольку программа центрального супервизора содержит 54 000 операторов ( в основном на языке ПЛ / 1), а механизмы защиты предусмотрены лишь частично, при реализации было решено упростить супервизор и разработать ряд механизмов защиты, которые можно было бы описать простыми, легкодоступными для понимания моделями. Затем была выполнена программная реализация супервизора и проведена его верификация. [17]
Рассмотрены девять направлений научных разработок по защите ЭВМ от несанкционированного доступа; исследование нарушений защиты системы; изучение связи пользователей с системой; верификация программ формирования математических моделей ядра защиты; исследование механизмов защиты от несанкционированного доступа в сетях передачи информации; средства защиты баз данных; механизмы установления полномочий пользователей, а также организационные аспекты обслуживания вычислительной системы Министерства обороны США. В конце статьи описаны разработки ряда ведущих организаций по данной тематике. [18]
Задачу верификации трех однопредикатных циклических программ ( типа whiledo, dountil, dowhiledo) можно свести к вопросу об их окончании и ( путем преобразования итерационных программ в рекурсивные) к верификации программ без циклов. [19]
А ], к-рый для программы А выражает модальность: необходимо после выполнения А. Центральные понятия верификация программ - понятия частичной и тотальной правильности программы А относительно предусловия Р и постусловия Q - выразимы формулами P [ A ] Q и P - ( [ A ] - ] Q) соответственно. [20]
Для любой применяемой на практике программы доказательство верифицируемое представляет собой более длинный алгоритм, чем алгоритм самой программы. Это делает процедуру верификации программы утомительной и подверженной многочисленным ошибкам. Неясно, однако, присуще ли это свойство только методу индуктивных утверждений или является общим ограничением любых методов верификации. [21]
Как и при рассмотрении верификации программ, эти условия не только оказываются логически более сильными, чем необходимые, но позволяют также выявить разумные с методологической точки зрения требования, которые следовало бы предъявлять к логическим алгоритмам. [22]
Кроме того, появляется меньше ошибок во время исполнения неправильных программ. Эта информация ценна и для верификации программ. В случае баз данных появляется богатое многообразие типов данных. Поэтому нужны дальнейшие исследования, чтобы объединить обшиость описания типов, имеющуюся в НОРЕ и ML, с богатством иерархии типов и подтипов, описываемых функциональной моделью данных и реляционной моделью, которые вводятся во второй половине этой книги. [23]
Многие термины, относящиеся к средствам числового программного управления, вычислительной технике и информатике, являются специфическими применительно к машиностроению. Они характеризуют, например; средства подготовки и верификации программ для станочной обработки, мониторинга технологических процессов, функции контрольно-управляющих устройств. [24]
Диапазон - это тип, который может содержать только ограниченное подмножество значений из полного множества значений указанного типа данных. Диапазоны полезны потому, что ограничение множества значений переменной предоставляет дополнительную возможность автоматической верификации программы, и потому, что диапазоны облегчают понимание программы. Диапазоны также важны потому, что их часто используют для объявления границ индексов массива. [25]
Дополнительные сложности возникают из-за ограничений, накладываемых машинной арифметикой, неопределенностью результатов и параллелизмом операций. Очень трудным делом может оказаться и разработка спецификации, согласно которой в дальнейшем будет проводиться верификация программы, дело в том, что невозможно показать правильность самой спецификации в смысле верного отображения замыслов разработчиков. Исследования, связанные с поиском способов доказательства правильности программ, внесли существенный вклад в программотехнику, где благодаря таким исследованиям удалось достичь лучшего понимания структуры алгоритмических языкое, принципов и методов программирования. Кроме того, масштабы практического применения формальных методов доказательства правильности программ постоянно расширяются и приобретают все большее значение. [26]
Структура языка программирования ( например, АДА [31]) дает возможность, используя аппарат пакетов и указаний ( прагм), сформировать основные разделы спецификации: описание входных и выходных параметров, типов, глобальных переменных, используемых пакетов, процедур и функций. Такая форма спецификаций позволяет при унификации языковых средств осуществить принципы нисходящего проектирования с возможностью предварительной оценки характеристик КП, а также верификацию программ. [27]
Предложенный Кларком для достижения этих целей подход полностью аналогичен подходу, который обычно применяется для анализа программ, написанных на других языках, и основывается, в частности, на различных видах индукции. Верификация программ посредством вывода их процедур была исследована вскоре после создания теории ВПО, и, по-видимому, это дает более простой метод доказательства частичной правильности. Сама возможность формализации большей части теории ВПО в логике первого порядка представляется важной для автоматизации обработки данных на метауровне. [28]
 |
Состав видов программного контроля данных. [29] |
Вновь разработанное и модифицированное программное обеспечение тестируют, используя контрольный пример. Это один из наиболее известных и применяемых способов проверки программ, несмотря на то что он достаточно трудоемок, дорог и не гарантирует правильность работы программы во всех режимах. В последнее время появились работы в области верификации программ, представляющей собой, в отличие от тестирования, основанного на выполнении операторов программы, аналитическую проверку ее свойств. [30]
Страницы: 1 2 3